Support for Coq v8.9

[tchajed]

On Coq v8.9 (and also on Coq master, coq/coq@2917fd2cce3a28), the plugin fails to build with the following error:

File "src/ast_plugin.ml4", line 439, characters 28-44:
Error: Unbound type constructor mutual_inductive

[ejgallego]

That's all you need for master

diff --git a/plugin/src/ast_plugin.ml4 b/plugin/src/ast_plugin.ml4
index d2d93b2..697290b 100644
--- a/plugin/src/ast_plugin.ml4
+++ b/plugin/src/ast_plugin.ml4
@@ -3,7 +3,6 @@ DECLARE PLUGIN "ast_plugin"
 open Format
 open Constr
 open Names
-open Stdarg
 open Environ
 open Declarations
 open Univ
@@ -247,9 +246,10 @@ let build_universe_instance (i : Instance.t) =
  * Build the AST for a sort
  *)
 let build_sort (s : Sorts.t) =
-  let s_ast =
+  let s_ast = let open Sorts in
     match s with
-    | Prop _ -> if s = Sorts.prop then "Prop" else "Set"
+    | Prop -> "Prop"
+    | Set -> "Set"
     | Type u -> build "Type" [build_universe u]
   in build "Sort" [s_ast]
 
@@ -436,7 +436,7 @@ let build_cofix (funs : string list) (index : int) =
 (*
  * Get the body of a mutually inductive type
  *)
-let lookup_mutind_body (i : mutual_inductive) (env : env) =
+let lookup_mutind_body (i : MutInd.t) (env : env) =
   lookup_mind i env
 
 (*

[tchajed]

Thanks for taking a look Emilio! It seems like let open Sorts does fix some warnings, but correctly handling Set correctly makes the plugin incompatible with Coq v8.8 so it should probably not be changed on the master branch. The current code coincidentally compiles on Coq v8.9 even though it will crash when printing Set and has an extra wildcard after Prop (which OCaml warns about but allows).

[ejgallego]

I strongly suggest that plugins do follow the upstream branching scheme [which I do on my own projects]

That is to say, master is supposed to work with the master branch, v8.9 with Coq's v8.9 etc...

This convention will be supported by Coq tools in the future [or course, people not wanting to follow it will have to define a few extra vars to indicate branch]

[ejgallego]

Note that GitHub has a feature to set default branch shown on the main project page.

[ejgallego]

The current code coincidentally compiles on Coq v8.9 even though it will crash when printing Set and has an extra wildcard after Prop (which OCaml warns about but allows).

I'm much afraid that this will make the plugin unusable, there is no choice other than branch. As of today I'm afraid that we are very far from having the same plugin code work in two versions of Coq.

And there are big API changes planned which mean that this will be more true. Maybe after 8.10 things are more stable, but now I'm afraid we have strong reasons for the API changes.