- Propagation des evars non résolues vers les with_bindings; permet par exemple

  de résoudre des buts comme celui-ci :

  Record nat_retract : Type := 
    {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
  Goal nat_retract.
  exists (fun x => x) (fun x => x).

- Nouvelle tentative d'utilisation des types des metas/evars pour
  inférer de nouvelles instances de metas/evars; permet par exemple
  d'utiliser f_equal sans option with, mais aussi, avec la modif
  précédente, de résoudre des buts tels que

  Goal exists f:bool->Prop, f true = True.
  exists (fun x => True).

  [Les expériences passées avaient montré qu'en prenant en compte les
  types dans l'unification, on peut unifier trop tôt une evars à une
  mauvaise sorte; à défaut de mécanisme de prise en compte des problème
  d'unification avec sous-typage, on s'est interdit ici d'unifier des
  types qui sont des arités.]

- Tout les constr de tactic_expr deviennent des open_constr (même si seul
  with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 25 insertions, 8 deletions

diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index ae3da9523a..169542e3cd 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -29,20 +29,37 @@ let pr_bindings prc prlc = function
         Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
   | Rawterm.NoBindings -> mt ()
 
-
 let pr_with_bindings prc prlc (c,bl) =
   prc c ++ hv 0 (pr_bindings prc prlc bl)
 
-
 let pr_fun_ind_using  prc prlc _ opt_c = 
   match opt_c with
     | None -> mt ()
     | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b))
 
+(* Duplication of printing functions because "'a with_bindings" is
+   (internally) not uniform in 'a: indeed constr_with_bindings at the
+   "typed" level has type "open_constr with_bindings" instead of
+   "constr with_bindings"; hence, its printer cannot be polymorphic in
+   (prc,prlc)... *)
+
+let pr_with_bindings_typed prc prlc (c,bl) =
+  prc c ++ 
+  hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c))  bl)
+
+let pr_fun_ind_using_typed prc prlc _ opt_c = 
+  match opt_c with
+    | None -> mt ()
+    | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b))
+
 
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings_opt
-  PRINTED BY pr_fun_ind_using
+  PRINTED BY pr_fun_ind_using_typed
+  RAW_TYPED AS constr_with_bindings_opt
+  RAW_PRINTED BY pr_fun_ind_using
+  GLOB_TYPED AS constr_with_bindings_opt
+  GLOB_PRINTED BY pr_fun_ind_using
 | [ "using" constr_with_bindings(c) ] -> [ Some c ]
 | [ ] -> [ None ]
 END
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 9ec02d4c48..fbf72805b7 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -23,13 +23,13 @@ open Hiddentac
 
 let pr_binding prc  = 
   function
-    | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
-    | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
 
 let pr_bindings prc prlc = function
   | Rawterm.ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
-      Util.prlist_with_sep spc prc l
+      Util.prlist_with_sep spc (fun (_,c) -> prc c) l
   | Rawterm.ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++ 
         Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
@@ -425,7 +425,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
-	     (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
+	     (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
 	  princ_infos.params
@@ -435,7 +435,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in 
-	     (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
+	     (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))