Merge pull request #72 from mattam82/revert-55-evar+strict_to_constr

Revert "[coq] Adapt to coq/coq#6454 "forbid calling to_constr on open terms""
mattam82 · Apr 13, 2018 · 8fb3d12 · 8fb3d12
2 parents a4b1c12 + 0e3bde6
commit 8fb3d12
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 16 deletions.
diff --git a/src/equations_common.ml b/src/equations_common.ml
@@ -970,8 +970,6 @@ let dest_ind_family fam =
   let ind, fam = Inductiveops.dest_ind_family fam in
   to_peuniverses ind, List.map of_constr fam
 
-(* XXX: EConstr-versions fo these functions really needed XXX *)
-let to_constr = to_constr ~abort_on_undefined_evars:false
 let prod_appvect sigma p args =
   of_constr (Term.prod_appvect (to_constr sigma p) (Array.map (to_constr sigma) args))
 let beta_appvect sigma p args =

diff --git a/src/noconf.ml b/src/noconf.ml
@@ -158,7 +158,7 @@ let derive_no_confusion env evd ~polymorphic (ind,u as indu) =
     Typeclasses.add_instance
       (Typeclasses.new_instance tc empty_hint_info true gr)
   in
-  let oblinfo, _, term, ty = Obligations.eterm_obligations env noid !evd 0 (to_constr ~abort_on_undefined_evars:false !evd term)
+  let oblinfo, _, term, ty = Obligations.eterm_obligations env noid !evd 0 (to_constr !evd term)
                                                            (to_constr !evd ty) in
     ignore(Obligations.add_definition ~hook:(Lemmas.mk_hook hook) packid 
 	      ~term ty ~tactic:(noconf_tac ()) 

diff --git a/src/sigma_types.ml b/src/sigma_types.ml
@@ -189,7 +189,8 @@ let build_sig_of_ind env sigma (ind,u as indu) =
   let sigma = !evd in
     sigma, pred, pars, fullapp, valsig, ctx, lenargs, idx
 
-let nf_econstr sigma c = Evarutil.nf_evar sigma c
+let nf_econstr sigma c =
+  EConstr.of_constr (EConstr.to_constr sigma c)
 
 let declare_sig_of_ind env sigma poly (ind,u) =
   let sigma, pred, pars, fullapp, valsig, ctx, lenargs, idx =
@@ -424,7 +425,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref)
   let rel_ty = Vars.lift rel rel_ty in
   let rel_t = Constr.mkRel rel in
   (* Fetch some information about the type of the variable being eliminated. *)
-  let pind, args = Inductive.find_inductive env (to_constr ~abort_on_undefined_evars:false !evd rel_ty) in
+  let pind, args = Inductive.find_inductive env (to_constr !evd rel_ty) in
   let mib, oib = Global.lookup_pinductive pind in
   let params, indices = List.chop mib.mind_nparams args in
   (* The variable itself will be treated for all purpose as one of its indices. *)
@@ -641,8 +642,8 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref)
   let params = List.map (Vars.lift (-(nb_cuts + oib.mind_nrealargs + 1))) params in
   let goal = Termops.it_mkProd_or_LetIn goal cuts_ctx in
   let goal = it_mkLambda_or_LetIn goal fresh_ctx in
-  let params = List.map (to_constr ~abort_on_undefined_evars:false !evd) params in
-  let goal' = to_constr ~abort_on_undefined_evars:false !evd goal in
+  let params = List.map (to_constr !evd) params in
+  let goal' = to_constr !evd goal in
   let branches_ty = Inductive.build_branches_type pind (mib, oib) params goal' in
   (* Refresh the inductive family. *)
   let indfam = Inductiveops.make_ind_family (pind, params) in

diff --git a/src/simplify.ml b/src/simplify.ml
@@ -271,7 +271,7 @@ let compose_term (env : Environ.env) (evd : Evd.evar_map ref)
         EConstr.mkVar id) named_ctx1 in
       (* Finally, substitute the rels in [c2] to get a valid term for [ev1]. *)
       let c2 = Vars.substl subst_ctx1 c2 in
-      evd := Evd.define ev1 (EConstr.to_constr ~abort_on_undefined_evars:false !evd c2) !evd;
+      evd := Evd.define ev1 (EConstr.to_constr !evd c2) !evd;
       evd := Evarsolve.check_evar_instance !evd ev1 c2 conv_fun;
       h2, c1
   | None -> assert false

diff --git a/src/splitting.ml b/src/splitting.ml
@@ -247,7 +247,7 @@ let term_of_tree status isevar env0 tree =
                   let env = Evd.evar_env ev_info in
                   Typing.type_of env evm term
                 in
-                evd := Evd.define (fst ev) (EConstr.to_constr ~abort_on_undefined_evars:false evm term) evm;
+                evd := Evd.define (fst ev) (EConstr.to_constr evm term) evm;
                 c
             (* This should not happen... *)
             | _ -> failwith "Should not fail here, please report."
@@ -377,10 +377,8 @@ let define_tree is_recursive fixprots poly impls status isevar env (i, sign, ari
   let _nf, _subst = Evarutil.e_nf_evars_and_universes isevar in
   let split = map_split (nf_evar !isevar) split in
   let obls, (emap, cmap), t', ty' =
-    (* XXX: EConstr Problem upstream indeed. *)
     Obligations.eterm_obligations env i !isevar
-      0 ~status (EConstr.to_constr ~abort_on_undefined_evars:false !isevar t)
-                (EConstr.to_constr ~abort_on_undefined_evars:false !isevar (whd_betalet !isevar ty))
+      0 ~status (EConstr.to_constr !isevar t) (EConstr.to_constr !isevar (whd_betalet !isevar ty))
   in
   let compobls = ref Id.Set.empty in
   let obls = 
@@ -469,6 +467,6 @@ let map_evars_in_constr evd evar_map c =
             let (f, uc) = Global.constr_of_global_in_context (Global.env ()) gr in
             let inst, ctx = ucontext_of_aucontext uc in
             Universes.constr_of_global_univ (Globnames.global_of_constr f, inst))
-           (EConstr.to_constr ~abort_on_undefined_evars:false evd c)
+           (EConstr.to_constr evd c)
 
 let map_evars_in_split evd m = map_split (map_evars_in_constr evd m)
diff --git a/src/subterm.ml b/src/subterm.ml
@@ -235,9 +235,7 @@ let derive_subterm env sigma ~polymorphic ind =
     let _ty' = Typing.e_type_of (Global.env ()) evm ty in
     let evm, nf = Evarutil.nf_evars_and_universes !evm in
     let obls, _, constr, typ =
-      Obligations.eterm_obligations env id evm 0
-        (to_constr ~abort_on_undefined_evars:false evm body)
-        (to_constr ~abort_on_undefined_evars:false evm ty)
+      Obligations.eterm_obligations env id evm 0 (to_constr evm body) (to_constr evm ty)
     in
     let ctx = Evd.evar_universe_context evm in
     Obligations.add_definition id ~term:constr typ ctx