- 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

8 files changed, 51 insertions, 34 deletions

diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 8eeb8b642..fac39df93 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -182,11 +182,11 @@ let right_instance_tac inst continue seq=
 	   [introf;
 	    (fun gls->
 	       split (Rawterm.ImplicitBindings 
-			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
+			[inj_open (mkVar (Tacmach.pf_nth_hyp_id gls 1))]) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption] 
     | Real ((0,t),_) ->
-	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	(tclTHEN (split (Rawterm.ImplicitBindings [inj_open t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index ae3da9523..169542e3c 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 9ec02d4c4..fbf72805b 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)))
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 48c9b9eb4..ab4da05e3 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -166,7 +166,7 @@ let rule_to_ntactic r =
    let rt =
      (match r with
        Nested(Tactic (t,_),_) -> t
-     | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
+     | Prim (Refine h) -> TacAtom (dummy_loc,TacExact (Tactics.inj_open h))
      | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
    if rule_is_complex r
    then (match rt with
@@ -1184,8 +1184,8 @@ let rec natural_ntree ig ntree =
 	  | TacIntroMove _ -> natural_intros ig lh g gs ltree
 	  | TacFix (_,n) -> natural_fix ig lh g gs n ltree
 	  | TacSplit (_,NoBindings) -> natural_split ig lh g gs ge [] ltree
-	  | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge l ltree
-	  | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree
+	  | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree
+	  | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd l) ltree
 	  | TacRight _ -> natural_right ig lh g gs ltree
 	  | TacLeft _ -> natural_left ig lh g gs ltree
 	  | (* "Simpl" *)TacReduce (r,cl)  ->
@@ -1202,17 +1202,17 @@ let rec natural_ntree ig ntree =
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
-	  | TacApply (false,(c,_)) -> natural_apply ig lh g gs c ltree
-	  | TacExact c -> natural_exact ig lh g gs c ltree
-	  | TacCut c -> natural_cut ig lh g gs c ltree
+	  | TacApply (false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
+	  | TacExact c -> natural_exact ig lh g gs (snd c) ltree
+	  | TacCut c -> natural_cut ig lh g gs (snd c) ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
 	      let _c = out_gen wit_constr a in
 	      natural_cutintro ig lh g gs a ltree
-	  | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false
+	  | TacCase (c,_) -> natural_case ig lh g gs ge (snd c) ltree false
 	  | TacExtend (_,"CaseIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_case ig lh g gs ge c ltree true
-	  | TacElim ((c,_),_) -> natural_elim ig lh g gs ge c ltree false
+	  | TacElim ((c,_),_) -> natural_elim ig lh g gs ge (snd c) ltree false
 	  | TacExtend (_,"ElimIntro",[a]) ->
 	      let c = out_gen wit_constr a in
 	      natural_elim ig lh g gs ge c ltree true
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
index 294943f7d..5fd763c36 100644
--- a/contrib/jprover/jprover.ml4
+++ b/contrib/jprover/jprover.ml4
@@ -410,7 +410,7 @@ i*)
      | Negl -> dyn_negl s1
      | Allr -> dyn_allr (JT.dest_var t2)
      | Alll -> dyn_alll s1 s2 (constr_of_jterm t2)
-     | Exr  -> dyn_exr (constr_of_jterm t2)
+     | Exr  -> dyn_exr (Tactics.inj_open (constr_of_jterm t2))
      | Exl  -> dyn_exl s1 s2 (JT.dest_var t2)
      | Ax -> T.assumption (*i TCL.tclIDTAC i*)
      | Truer -> dyn_truer
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 951378d4b..497fcdb6c 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1221,7 +1221,7 @@ let replay_history tactic_normalisation =
 	      (clear [aux]);
 	      (intros_using [id]);
 	      (loop l) ];
-            tclTHEN (exists_tac eq1) reflexivity ]
+            tclTHEN (exists_tac (inj_open eq1)) reflexivity ]
       | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
 	  let id1 = new_identifier () 
 	  and id2 = new_identifier () in
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 7a2133a02..49791c367 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -416,8 +416,8 @@ let base_leaf_terminate (func:global_reference) eqs expr =
 	   [k';h] -> k',h
 	 | _ -> assert false
      in
-     tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [expr]));
-		  observe_tac "second split" (split (ImplicitBindings [delayed_force coq_O]));
+     tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [inj_open expr]));
+		  observe_tac "second split" (split (ImplicitBindings [inj_open (delayed_force coq_O)]));
 		  observe_tac "intro k" (h_intro k');
                   observe_tac "case on k" 
 		      (tclTHENS 
@@ -459,7 +459,7 @@ let rec compute_le_proofs = function
 	      in
 	      apply_with_bindings
 		(le_trans,
-		 ExplicitBindings[dummy_loc,NamedHyp m_id,a])
+		 ExplicitBindings[dummy_loc,NamedHyp m_id,inj_open a])
 		g
 	   )
 	   [compute_le_proofs tl; 
@@ -477,7 +477,7 @@ let make_lt_proof pmax le_proof =
        in
        apply_with_bindings
 	 (le_lt_trans,
-	  ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g)
+	  ExplicitBindings[dummy_loc,NamedHyp m_id, inj_open pmax]) g)
     [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); 
      tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];;
 
@@ -496,8 +496,8 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	 tclTHENS
 	   (general_rewrite_bindings false
 	      (mkVar eq,
-	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
-				dummy_loc, NamedHyp def_id, mkVar def]) false)
+	       ExplicitBindings[dummy_loc, NamedHyp k_id, inj_open (mkVar k);
+				dummy_loc, NamedHyp def_id, inj_open (mkVar def)]) false)
 	   [list_cond_rewrite k def pmax eqs le_proofs;
             observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
       ) 
@@ -515,7 +515,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
         let ids = h'::ids in
 	let def = next_global_ident_away true def_id ids in
 	tclTHENLIST
-	  [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
+	  [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [inj_open s_max]));
 	   observe_tac "introduce_all_equalities_final intro k" (h_intro  k);
 	   tclTHENS
 	     (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k)))
@@ -575,8 +575,8 @@ let rec introduce_all_values is_mes acc_inv func context_fn
     (match args with
     [] -> 
       tclTHENLIST
-	[observe_tac "split" (split(ImplicitBindings
-		 [context_fn (List.map mkVar (List.rev values))]));
+	[observe_tac "split" (split(ImplicitBindings 
+		 [inj_open (context_fn (List.map mkVar (List.rev values)))]));
 	 observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs
 	   (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
   | arg::args ->
@@ -1194,9 +1194,9 @@ let rec introduce_all_values_eq  cont_tac functional termine
 		general_rewrite_bindings false
 		(mkVar heq1,
 		 ExplicitBindings[dummy_loc,NamedHyp k_id,
-				  f_S(f_S(mkVar pmax));
+		                  inj_open (f_S(f_S(mkVar pmax)));
 				  dummy_loc,NamedHyp def_id,
-				  f]) false gls )
+				  inj_open f]) false gls )
 	     [tclTHENLIST
 		[simpl_iter();
 		 unfold_constr (reference_of_constr functional);
@@ -1247,8 +1247,8 @@ let rec introduce_all_values_eq  cont_tac functional termine
 			   (mkVar heq,
 			    ExplicitBindings
 			      [dummy_loc, NamedHyp k_id,
-			       f_S(mkVar pmax');
-			       dummy_loc, NamedHyp def_id, f]) false))
+			       inj_open (f_S(mkVar pmax'));
+			       dummy_loc, NamedHyp def_id, inj_open f]) false))
 			   g
 		     )
 		     [tclIDTAC;
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index fb58a14eb..5a32d2e42 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -231,7 +231,7 @@ let build_dependent_sum l =
 		([intros;
 		  (tclTHENSEQ 
 		     [constructor_tac (Some 1) 1 
-			(Rawterm.ImplicitBindings [mkVar n]);
+			(Rawterm.ImplicitBindings [inj_open (mkVar n)]);
 		      cont]);
 		 ])))
 	in