Removing some return type compatibility layers in Termops.

11 files changed, 44 insertions, 42 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0d48b65d0..7a99c45a8 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -63,7 +63,6 @@ let rec decompose_term env sigma t=
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
     | Prod (_,a,_b) when noccurn sigma 1 _b ->
 	let b = Termops.pop _b in
-	let b = EConstr.of_constr b in
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	Appli(Appli(Product (sort_a,sort_b) ,
@@ -118,7 +117,6 @@ let rec pattern_of_constr env sigma c =
 	List.fold_left Int.Set.union Int.Set.empty lrels
     | Prod (_,a,_b) when noccurn sigma 1 _b ->
 	let b = Termops.pop _b in
-	let b = EConstr.of_constr b in
 	let pa,sa = pattern_of_constr env sigma a in
 	let pb,sb = pattern_of_constr env sigma b in
 	let sort_b = sf_of env sigma b in
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index ddf013735..ae057b458 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -374,7 +374,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
     match st'.st_it with
 	Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
       | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
-  let thyps = fst (match_hyps blend nam2 (Termops.pop (EConstr.of_constr rest1)) hyps) in
+  let thyps = fst (match_hyps blend nam2 (Vars.lift (-1) rest1) hyps) in
     tparams,{pat_vars=tpatvars;
 	     pat_aliases=taliases;
 	     pat_constr=pat_pat;
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 96b991e1f..87bac2fe3 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -76,11 +76,13 @@ type kind_of_formula=
   | Forall of constr*constr
   | Atom of constr
 
+let pop t = Vars.lift (-1) t
+
 let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
     match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with
-	Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop b))
+	Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b)))
       |_->
 	 match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with
 	     Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b)
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 5520c7e35..7cbfb8e7d 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -24,6 +24,8 @@ exception UFAIL of constr*constr
 let strip_outer_cast t =
   EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *)
 
+let pop t = Vars.lift (-1) t
+
 let unif t1 t2=
   let evd = Evd.empty in (** FIXME *)
   let bige=Queue.create ()
@@ -62,7 +64,7 @@ let unif t1 t2=
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
-	      Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige
+	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
 	      Queue.add (pa,pb) bige;
 	      Queue.add (ca,cb) bige;
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 188368082..cc29d68f5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -95,6 +95,7 @@ let list_chop ?(msg="") n l =
   with Failure (msg') ->
     failwith (msg ^ msg')
 
+let pop t = Vars.lift (-1) t
 
 let make_refl_eq constructor type_of_t t  =
 (*   let refl_equal_term = Lazy.force refl_equal in *)
@@ -289,7 +290,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
     in
     let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
-    let end_of_type_with_pop = Termops.pop (EConstr.of_constr end_of_type) in (*the equation will be removed *)
+    let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
     let new_end_of_type =
       (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
@@ -311,9 +312,9 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	   try
 	     let witness = Int.Map.find i sub in
 	     if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
-	     (Termops.pop (EConstr.of_constr end_of_type),ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
+	     (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
 	   with Not_found  ->
-	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
+	     (Term.mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
 	1
 	(new_end_of_type,0,witness_fun)
@@ -416,7 +417,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
   let coq_I = Coqlib.build_coq_I () in
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn type_of_hyp then
-      let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
+      let real_type_of_hyp = Term.it_mkProd_or_LetIn type_of_hyp context in
       let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
       (* length of context didn't change ? *)
       let new_context,new_typ_of_hyp =
@@ -429,13 +430,13 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
     then
       begin
 	let (x,t_x,t') = destProd type_of_hyp in
-	let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in
+	let actual_real_type_of_hyp = Term.it_mkProd_or_LetIn t' context in
 	if is_property ptes_infos t_x actual_real_type_of_hyp then
 	  begin
 	    let pte,pte_args =  (destApp t_x) in
 	    let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in
-	    let popped_t' = Termops.pop (EConstr.of_constr t') in
-	    let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
+	    let popped_t' = pop t' in
+	    let real_type_of_hyp = Term.it_mkProd_or_LetIn popped_t' context in
 	    let prove_new_type_of_hyp =
 	      let context_length = List.length context in
 	      tclTHENLIST
@@ -486,9 +487,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 (* 	    observe (str "In "++Ppconstr.pr_id hyp_id++  *)
 (* 		       str " removing useless precond True" *)
 (* 		    );  *)
-	  let popped_t' = Termops.pop (EConstr.of_constr t') in
+	  let popped_t' = pop t' in
 	  let real_type_of_hyp =
-	    it_mkProd_or_LetIn popped_t' context
+	    Term.it_mkProd_or_LetIn popped_t' context
 	  in
 	  let prove_trivial =
 	    let nb_intro = List.length context in
@@ -515,9 +516,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	  ]
 	else if is_trivial_eq t_x
 	then (*  t_x :=  t = t   => we remove this precond *)
-	  let popped_t' = Termops.pop (EConstr.of_constr t') in
+	  let popped_t' = pop t' in
 	  let real_type_of_hyp =
-	    it_mkProd_or_LetIn popped_t' context
+	    Term.it_mkProd_or_LetIn popped_t' context
 	  in
 	  let hd,args = destApp t_x in
 	  let get_args hd args =
@@ -616,8 +617,8 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	 let fun_body =
 	   mkLambda(Anonymous,
 		    pf_unsafe_type_of g' term,
-		    Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
-		   )
+		    EConstr.Unsafe.to_constr (Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
+		   ))
 	 in
 	 let new_body = pf_nf_betaiota g' (EConstr.of_constr (mkApp(fun_body,[| new_term_value |]))) in
 	 let new_body = EConstr.Unsafe.to_constr new_body in
@@ -988,7 +989,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       (nb_params + nb_args) t,evd
   in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
-  let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
+  let lemma_type = Term.it_mkProd_or_LetIn eqn type_ctxt in
   (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
   let f_id = Label.to_id (con_label (fst (destConst f))) in
   let prove_replacement =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b4eb77870..8683f68c6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -23,6 +23,8 @@ let observe s =
   if do_observe ()
   then Feedback.msg_debug s
 
+let pop t = Vars.lift (-1) t
+
 (*
    Transform an inductive induction principle into
    a functional one
@@ -111,7 +113,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let dummy_var = mkVar (Id.of_string "________") in
   let mk_replacement c i args =
-    let res = mkApp(rel_to_fun.(i), Array.map (fun c -> Termops.pop (EConstr.of_constr c)) (array_get_start args)) in
+    let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in
     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res);
     res
   in
@@ -169,25 +171,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_env = Environ.push_rel (LocalAssum (x,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	 then (Termops.pop (EConstr.of_constr new_b)), filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+	 then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
 	 else
 	   (
 	     bind_fun(new_x,new_t,new_b),
 	     list_union_eq
 	       eq_constr
 	       binders_to_remove_from_t
-	       (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+	       (List.map pop binders_to_remove_from_b)
 	   )
 
        with
 	 | Toberemoved ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
@@ -198,25 +200,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (Termops.pop (EConstr.of_constr new_b)),filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
 	else
 	  (
 	    mkLetIn(new_x,new_v,new_t,new_b),
 	    list_union_eq
 	      eq_constr
 	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
-	      (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+	      (List.map pop binders_to_remove_from_b)
 	  )
 
       with
 	| Toberemoved ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
     let new_e,to_remove_from_e = compute_new_princ_type remove env e
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c02b64c1f..ca066c4cc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -399,8 +399,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	   match ctxt with
 	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::decl::ctxt ->
-		let res = Termops.it_mkLambda_or_LetIn
-			    (Termops.it_mkProd_or_LetIn concl [hres;res])
+		let res = Term.it_mkLambda_or_LetIn
+			    (Term.it_mkProd_or_LetIn concl [hres;res])
 			    (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
 		in
 		res
@@ -793,7 +793,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 in
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
-	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+	 let type_of_lemma = Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
 	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
 	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	   let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
@@ -861,7 +861,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma =
-	   Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
+	   Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
 	 let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	 let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 3688b8c15..2840193a9 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -32,7 +32,8 @@ module RelDecl = Context.Rel.Declaration
 
 (** {2 Useful operations on constr and glob_constr} *)
 
-let rec popn i c = if i<=0 then c else EConstr.of_constr (pop (popn (i-1) c))
+let pop c = Vars.lift (-1) c
+let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
 
 (** Substitutions in constr *)
 let compare_constr_nosub t1 t2 =
@@ -986,13 +987,13 @@ let relprinctype_to_funprinctype relprinctype nfuns =
   (* first remove indarg and indarg_in_concl *)
   let relinfo_noindarg = { relinfo with
     indarg_in_concl = false; indarg = None;
-    concl = EConstr.of_constr (remove_last_arg (pop relinfo.concl)); } in
+    concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in
   (* the nfuns last induction arguments are functional ones: remove them *)
   let relinfo_argsok = { relinfo_noindarg with
     nargs = relinfo_noindarg.nargs - nfuns;
     (* args is in reverse order, so remove fst *)
     args = remove_n_fst_list nfuns relinfo_noindarg.args;
-    concl = popn nfuns relinfo_noindarg.concl;
+    concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl));
   } in
   let new_branches =
     List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c71174fef..23b308efb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -408,6 +408,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 		args.(1),args.(2)
 	      in
 	      let new_b' = Termops.replace_term (project g') (EConstr.of_constr teq_lhs) (EConstr.of_constr teq_rhs) (EConstr.of_constr new_b) in 
+	      let new_b' = EConstr.Unsafe.to_constr new_b' in
 	      let new_infos = {
 		infos with 
 		  info = new_b';
@@ -1253,7 +1254,7 @@ let clear_goals =
       | Prod(Name id as na,t',b) ->
 	  let b' = clear_goal b in
 	  if noccurn 1 b' && (is_rec_res id)
-	  then Termops.pop (EConstr.of_constr b')
+	  then Vars.lift (-1) b'
 	  else if b' == b then t
 	  else mkProd(na,t',b')
       | _ -> Term.map_constr clear_goal t
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2ad97c75b..87276f5df 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -270,7 +270,7 @@ let compute_ivs f cs gl =
 
 	      (* The Cases predicate is a lambda; we assume no dependency *)
 	      let p = match EConstr.kind sigma p with
-		| Lambda (_,_,p) -> EConstr.of_constr (Termops.pop p)
+		| Lambda (_,_,p) -> Termops.pop p
 		| _ -> p
 	      in
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 63eccaa40..131ecad33 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -246,7 +246,6 @@ let lapp f args = mkApp(Lazy.force f,args)
 
 let plapp evd f args = 
   let fc = Evarutil.e_new_global evd (Lazy.force f) in
-  let fc = EConstr.of_constr fc in
     mkApp(fc,args)
 
 let dest_rel0 sigma t =
@@ -591,7 +590,6 @@ let make_hyp env evd c =
 
 let make_hyp_list env evd lH =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
-  let carrier = EConstr.of_constr carrier in
   let l = 
     List.fold_right
       (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
@@ -602,7 +600,6 @@ let make_hyp_list env evd lH =
 
 let interp_power env evd pow =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
-  let carrier = EConstr.of_constr carrier in
   match pow with
   | None ->
       let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
@@ -618,7 +615,6 @@ let interp_power env evd pow =
 
 let interp_sign env evd sign =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
-  let carrier = EConstr.of_constr carrier in
   match sign with
   | None -> plapp evd coq_None [|carrier|]
   | Some spec ->
@@ -628,7 +624,6 @@ let interp_sign env evd sign =
 
 let interp_div env evd div =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
-  let carrier = EConstr.of_constr carrier in
   match div with
   | None -> plapp evd coq_None [|carrier|]
   | Some spec ->