Introducing contexts parameterized by the inner term type.

This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.

3 files changed, 37 insertions, 39 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a4b6cb53b7..ef67d28f9c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -939,7 +939,7 @@ module Search = struct
     let cwd = Lib.cwd () in
     if DirPath.equal cwd dir &&
          (onlyc == only_classes) &&
-           Context.Named.equal sign sign' &&
+           Context.Named.equal Constr.equal sign sign' &&
              Hint_db.transparent_state cached_hints == st
     then cached_hints
     else
@@ -1034,7 +1034,7 @@ module Search = struct
             (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
                pr_ev s' (Proofview.Goal.goal gl'));
         let hints' =
-          if b && not (Context.Named.equal (Goal.hyps gl') (Goal.hyps gl))
+          if b && not (Context.Named.equal Constr.equal (Goal.hyps gl') (Goal.hyps gl))
           then
             let st = Hint_db.transparent_state info.search_hints in
             make_autogoal_hints info.search_only_classes ~st gl'
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 855273d3bf..188e215a5d 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -73,8 +73,8 @@ let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (mkIndU ind,
-       Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt
-       @ Context.Rel.to_extended_list 0 realargs)
+       Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
+       @ Context.Rel.to_extended_list mkRel 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
 let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s
@@ -172,7 +172,7 @@ let build_sym_scheme env ind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
@@ -185,7 +185,7 @@ let build_sym_scheme env ind =
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkApp (mkIndU indu,Array.concat
-	  [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+	  [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 	   rel_vect 1 nrealargs;
 	   rel_vect (2*nrealargs+2) nrealargs])),
      mkRel 1 (* varH *),
@@ -226,13 +226,13 @@ let build_sym_involutive_scheme env ind =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
-  let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in
+  let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
       (mkIndU indu, Array.append
-         (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt)
+         (Context.Rel.to_extended_vect mkRel (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
     name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
@@ -246,15 +246,15 @@ let build_sym_involutive_scheme env ind =
 	       (mkApp (eq,[|
 	       mkApp
 	       (mkIndU indu, Array.concat
-	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 		rel_vect (2*nrealargs+2) nrealargs;
 		rel_vect 1 nrealargs]);
                mkApp (sym,Array.concat
-	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 		rel_vect 1 nrealargs;
 		rel_vect (2*nrealargs+2) nrealargs;
 		[|mkApp (sym,Array.concat
-		[Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+		[Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 		 rel_vect (2*nrealargs+2) nrealargs;
 		 rel_vect 1 nrealargs;
 		 [|mkRel 1|]])|]]);
@@ -337,7 +337,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -345,12 +345,12 @@ let build_l2r_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (3*nrealargs) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect nrealargs nrealargs]) in
   let applied_ind_G =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (3*nrealargs+3) paramsctxt1;
         rel_vect (nrealargs+3) nrealargs;
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
@@ -361,10 +361,10 @@ let build_l2r_rew_scheme dep env ind kind =
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
-       Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
+       Array.append (Context.Rel.to_extended_vect mkRel n mip.mind_arity_ctxt) [|mkVar varH|]) in
   let applied_sym_G =
      mkApp(sym,
-       Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1;
+       Array.concat [Context.Rel.to_extended_vect mkRel (nrealargs*3+4) paramsctxt1;
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
@@ -374,7 +374,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
   let applied_PC =
-    mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign)
+    mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect mkRel 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
   let applied_PG =
     mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs)
@@ -384,11 +384,11 @@ let build_l2r_rew_scheme dep env ind kind =
            (if dep then [|mkRel 2|] else [||])) in
   let applied_sym_sym =
          mkApp (sym,Array.concat
-	   [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
+	   [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
             rel_vect 4 nrealargs;
             rel_vect (nrealargs+4) nrealargs;
             [|mkApp (sym,Array.concat
-	      [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
+	      [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
 	       rel_vect (nrealargs+4) nrealargs;
 	       rel_vect 4 nrealargs;
 	       [|mkRel 2|]])|]]) in
@@ -411,7 +411,7 @@ let build_l2r_rew_scheme dep env ind kind =
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
                    applied_PR)),
        mkApp (sym_involutive,
-         Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
+         Array.append (Context.Rel.to_extended_vect mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]),
        [|main_body|])
    else
      main_body))))))
@@ -450,7 +450,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     get_sym_eq_data env indu in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -458,12 +458,12 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (4*nrealargs+2) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (nrealargs+1) nrealargs]) in
   let applied_ind_P' =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (3*nrealargs+1) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
@@ -541,7 +541,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
     get_non_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -557,8 +557,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
   let applied_PG =
     mkApp (mkVar varP,
-           if dep then Context.Rel.to_extended_vect 0 realsign_ind
-	   else Context.Rel.to_extended_vect 1 realsign) in
+           if dep then Context.Rel.to_extended_vect mkRel 0 realsign_ind
+	   else Context.Rel.to_extended_vect mkRel 1 realsign) in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
@@ -608,7 +608,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
 	    (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
 	      (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty
 		(EConstr.of_constr (applist (c,
-	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
+	          Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
       in c', ctx'
   | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
@@ -763,8 +763,8 @@ let build_congr env (eq,refl,ctx) ind =
      (mkNamedLambda varH
         (applist
            (mkIndU indu,
-	    Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @
-	    Context.Rel.to_extended_list 0 realsign))
+	    Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
+	    Context.Rel.to_extended_list mkRel 0 realsign))
      (mkCase (ci,
        my_it_mkLambda_or_LetIn_name
 	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
@@ -772,9 +772,9 @@ let build_congr env (eq,refl,ctx) ind =
            (Anonymous,
             applist
              (mkIndU indu,
-	        Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3)
+	        Context.Rel.to_extended_list mkRel (2*mip.mind_nrealdecls+3)
 		  paramsctxt
-	        @ Context.Rel.to_extended_list 0 realsign),
+	        @ Context.Rel.to_extended_list mkRel 0 realsign),
             mkApp (eq,
 	      [|mkVar varB;
                 mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0ecccd5c02..8260c14ad4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1634,7 +1634,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       then
         let t = lift (i+1-n) t in
 	let abselim = beta_applist sigma (elim, params@[t;branch]) in
-	let args = Array.map EConstr.of_constr (Context.Rel.to_extended_vect 0 sign) in
+	let args = Context.Rel.to_extended_vect mkRel 0 sign in
 	let c = beta_applist sigma (abselim, [mkApp (c, args)]) in
 	  Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
       else
@@ -1643,8 +1643,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       (* goes from left to right when i increases! *)
       match List.nth l i with
       | Some proj ->
-	  let args = Context.Rel.to_extended_vect 0 sign in
-	  let args = Array.map EConstr.of_constr args in
+	  let args = Context.Rel.to_extended_vect mkRel 0 sign in
 	  let proj =
 	    if Environ.is_projection proj env then
 	      mkProj (Projection.make proj false, mkApp (c, args))
@@ -2190,7 +2189,7 @@ let bring_hyps hyps =
       let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
-      let args = Array.map_of_list EConstr.of_constr (Context.Named.to_instance hyps) in
+      let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
       Refine.refine { run = begin fun sigma ->
         let Sigma (ev, sigma, p) =
           Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -2868,8 +2867,7 @@ let old_generalize_dep ?(with_let=false) c gl =
     (cl',project gl) in
   (** Check that the generalization is indeed well-typed *)
   let (evd, _) = Typing.type_of env evd cl'' in
-  let args = Context.Named.to_instance to_quantify_rev in
-  let args = List.map EConstr.of_constr args in
+  let args = Context.Named.to_instance mkVar to_quantify_rev in
   tclTHENLIST
     [tclEVARS evd;
      Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
@@ -3994,7 +3992,7 @@ let compute_scheme_signature evd scheme names_info ind_type_guess =
 	    let ind_is_ok =
 	      List.equal (fun c1 c2 -> EConstr.eq_constr evd c1 c2)
 		(List.lastn scheme.nargs indargs)
-		(List.map EConstr.of_constr (Context.Rel.to_extended_list 0 scheme.args)) in
+		(Context.Rel.to_extended_list mkRel 0 scheme.args) in
 	    if not (ccl_arg_ok && ind_is_ok) then
 	      error_ind_scheme "the conclusion of"
 	  in (cond, check_concl)
@@ -4965,7 +4963,7 @@ let abstract_subproof id gk tac =
   in
   let const, args =
     if !shrink_abstract then shrink_entry sign const
-    else (const, List.rev (Context.Named.to_instance sign))
+    else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
   in
   let args = List.map EConstr.of_constr args in
   let cd = Entries.DefinitionEntry const in