Coq tactic: fixed bug related to order of type parameters

Makefile.in

@@ -838,6 +838,12 @@ src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
 	    WHY3NOCONFIG=42 $(COQC) -opt -I lib/coq-tactic/ $< && \
 	    touch src/coq-tactic/.why3-vo-opt
 
+test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
+	$(COQC) -byte -I lib/coq-tactic/ src/coq-tactic/test.v
+
+test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
+	$(COQC) -opt -I lib/coq-tactic/ src/coq-tactic/test.v
+
 # depend and clean targets
 
 ifneq "$(MAKECMDGOALS)" "clean"
@@ -1025,6 +1031,9 @@ install_local: bin/why3doc
 bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
 	$(MAKE) test-api.@OCAMLBEST@
 	sh bench/bench "bin/why3.@OCAMLBEST@" "bin/why3ml.@OCAMLBEST@"
+	@if test "@enable_coq_plugin@" = "yes"; then \
+	   echo "=== checking the Coq tactic ==="; \
+	   $(MAKE) test-coq-tactic.@OCAMLBEST@; fi
 
 ###############
 # test targets

src/coq-tactic/test.v

@@ -28,11 +28,6 @@ with forest : Set :=
   | Nil : forest
   | Cons : tree -> forest -> forest.
 
-Print plus.
-
-Print tree_rect.
-
-
 Fixpoint tree_size (t:tree) : Z := match t with
   | Leaf => 0
   | Node _ f => 1 + forest_size f end
@@ -129,14 +124,10 @@ Qed.
 
 End S.
 
-Print All.
-
 Goal True.
 ae.
 Qed.
 
-Print sorted.
-
 Goal sorted _ (@nil nat).
 ae.
 Qed.
@@ -178,8 +169,6 @@ Goal p' O.
 ae.
 Qed.
 
-Print plus.
-
 Goal plus O O = O.
 ae.
 Qed.
@@ -227,8 +216,6 @@ Qed.
 
 (* recursive predicate definition *)
 
-Print In.
-
 Goal In 0 (cons 1 (cons 0 nil)).
 ae.
 Qed.
@@ -324,3 +311,14 @@ Goal forall x : ptree' Z, x=x.
 ae.
 Qed.
 
+(* order of type parameters matters *)
+
+Definition wgt (k:(nat * Z)%type) := match k with
+  | (_, p) => p
+  end.
+Implicit Arguments wgt.
+
+Goal wgt (S O, 3) = 3.
+ae.
+Qed.
+

src/coq-tactic/why3tac.ml

@@ -182,7 +182,8 @@ let decomp_type_quantifiers env t =
           let tv = Ty.create_tvsymbol (preid_of_id id) in
           Idmap.add id (Some (Ty.ty_var tv)) m, tv
         in
-        Util.map_fold_left add Idmap.empty vars, env, t
+        let tvm, vars = Util.map_fold_left add Idmap.empty vars in
+        (tvm, List.rev vars), env, t
   in
   loop [] t