Removing some return type compatibility layers in Termops.

1 files changed, 11 insertions, 9 deletions

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