Termops API using EConstr.

6 files changed, 41 insertions, 41 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fad656223..34bc83097 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -77,7 +77,7 @@ let clenv_push_prod cl =
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
 	let mv = new_meta () in
-	let dep = dependent (mkRel 1) u in
+	let dep = not (EConstr.Vars.noccurn (cl_sigma cl) 1 (EConstr.of_constr u)) in
 	let na' = if dep then na else Anonymous in
 	let e' = meta_declare mv t ~name:na' cl.evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
@@ -332,7 +332,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta ty then fold clenv (mvs@[mv])
+      if occur_meta clenv.evd (EConstr.of_constr ty) then fold clenv (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
@@ -404,7 +404,7 @@ type arg_bindings = constr explicit_bindings
  * of cval, ctyp. *)
 
 let clenv_independent clenv =
-  let mvs = collect_metas (clenv_value clenv) in
+  let mvs = collect_metas clenv.evd (EConstr.of_constr (clenv_value clenv)) in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
@@ -522,7 +522,7 @@ let clenv_match_args bl clenv =
 exception NoSuchBinding
 
 let clenv_constrain_last_binding c clenv =
-  let all_mvs = collect_metas clenv.templval.rebus in
+  let all_mvs = collect_metas clenv.evd (EConstr.of_constr clenv.templval.rebus) in
   let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k c
 
@@ -612,7 +612,7 @@ let make_evar_clause env sigma ?len t =
       let sigma = Sigma.Unsafe.of_evar_map sigma in
       let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
       let sigma = Sigma.to_evar_map sigma in
-      let dep = dependent (mkRel 1) t2 in
+      let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in
       let hole = {
         hole_evar = ev;
         hole_type = t1;
@@ -682,9 +682,9 @@ let solve_evar_clause env sigma hyp_only clause = function
     if h.hole_deps then
       (** Some subsequent term uses the hole *)
       let (ev, _) = destEvar h.hole_evar in
-      let is_dep hole = occur_evar ev hole.hole_type in
+      let is_dep hole = occur_evar sigma ev (EConstr.of_constr hole.hole_type) in
       let in_hyp = List.exists is_dep holes in
-      let in_ccl = occur_evar ev clause.cl_concl in
+      let in_ccl = occur_evar sigma ev (EConstr.of_constr clause.cl_concl) in
       let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
       let h = { h with hole_deps = dep } in
       h :: holes
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 98b5bc8b0..d8a20e08b 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -33,12 +33,12 @@ let clenv_cast_meta clenv =
       | _  -> map_constr crec u
 
   and crec_hd u =
-    match kind_of_term (strip_outer_cast u) with
+    match kind_of_term (strip_outer_cast clenv.evd (EConstr.of_constr u)) with
       | Meta mv ->
 	  (try
             let b = Typing.meta_type clenv.evd mv in
-	    assert (not (occur_meta b));
-	    if occur_meta b then u
+	    assert (not (occur_meta clenv.evd (EConstr.of_constr b)));
+	    if occur_meta clenv.evd (EConstr.of_constr b) then u
             else mkCast (mkMeta mv, DEFAULTcast, b)
 	  with Not_found -> u)
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index ff0df9179..d4b308bbe 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -25,7 +25,7 @@ let depends_on_evar evk _ (pbty,_,t1,t2) =
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c env evd =
-  if Termops.occur_evar evk c then
+  if Termops.occur_evar evd evk (EConstr.of_constr c) then
     Pretype_errors.error_occur_check env evd evk c;
   let evd = define evk c evd in
   let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 44c629484..29f295682 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -138,12 +138,12 @@ let find_q x (m,q) =
         else find (Id.Set.union l accs) (i::acc) itl in
   find Id.Set.empty [] q
 
-let occur_vars_in_decl env hyps d =
+let occur_vars_in_decl env sigma hyps d =
   if Id.Set.is_empty hyps then false else
-    let ohyps = global_vars_set_of_decl env d in
+    let ohyps = global_vars_set_of_decl env sigma d in
     Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps
 
-let reorder_context env sign ord =
+let reorder_context env sigma sign ord =
   let ords = List.fold_right Id.Set.add ord Id.Set.empty in
   if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
     error "Order list has duplicates";
@@ -152,13 +152,13 @@ let reorder_context env sign ord =
       | [] -> List.rev ctxt_tail @ ctxt_head
       | top::ord' when mem_q top moved_hyps ->
           let ((d,h),mh) = find_q top moved_hyps in
-          if occur_vars_in_decl env h d then
+          if occur_vars_in_decl env sigma h d then
             user_err ~hdr:"reorder_context"
               (str "Cannot move declaration " ++ pr_id top ++ spc() ++
               str "before " ++
               pr_sequence pr_id
                 (Id.Set.elements (Id.Set.inter h
-                  (global_vars_set_of_decl env d))));
+                  (global_vars_set_of_decl env sigma d))));
           step ord' expected ctxt_head mh (d::ctxt_tail)
       | _ ->
           (match ctxt_head with
@@ -173,16 +173,16 @@ let reorder_context env sign ord =
                     ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
   step ord ords sign mt_q []
 
-let reorder_val_context env sign ord =
-  val_of_named_context (reorder_context env (named_context_of_val sign) ord)
+let reorder_val_context env sigma sign ord =
+  val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord)
 
 
 
 
-let check_decl_position env sign d =
+let check_decl_position env sigma sign d =
   let x = NamedDecl.get_id d in
-  let needed = global_vars_set_of_decl env d in
-  let deps = dependency_closure env (named_context_of_val sign) needed in
+  let needed = global_vars_set_of_decl env sigma d in
+  let deps = dependency_closure env sigma (named_context_of_val sign) needed in
   if Id.List.mem x deps then
     user_err ~hdr:"Logic.check_decl_position"
       (str "Cannot create self-referring hypothesis " ++ pr_id x);
@@ -233,12 +233,12 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp toleft (left,declfrom,right) hto =
+let move_hyp sigma toleft (left,declfrom,right) hto =
   let env = Global.env() in
   let test_dep d d2 =
     if toleft
-    then occur_var_in_decl env (NamedDecl.get_id d2) d
-    else occur_var_in_decl env (NamedDecl.get_id d) d2
+    then occur_var_in_decl env sigma (NamedDecl.get_id d2) d
+    else occur_var_in_decl env sigma (NamedDecl.get_id d) d2
   in
   let rec moverec first middle = function
     | [] ->
@@ -278,10 +278,10 @@ let move_hyp toleft (left,declfrom,right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
-let move_hyp_in_named_context hfrom hto sign =
+let move_hyp_in_named_context sigma hfrom hto sign =
   let (left,right,declfrom,toleft) =
     split_sign hfrom hto (named_context_of_val sign) in
-  move_hyp toleft (left,declfrom,right) hto
+  move_hyp sigma toleft (left,declfrom,right) hto
 
 (**********************************************************************)
 
@@ -320,10 +320,10 @@ let check_conv_leq_goal env sigma arg ty conclty =
   else sigma
 
 exception Stop of constr list
-let meta_free_prefix a =
+let meta_free_prefix sigma a =
   try
     let _ = Array.fold_left (fun acc a -> 
-      if occur_meta a then raise (Stop acc)
+      if occur_meta sigma (EConstr.of_constr a) then raise (Stop acc)
       else a :: acc) [] a
     in a
   with Stop acc -> Array.rev_of_list acc
@@ -338,7 +338,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   let mk_goal hyps concl =
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
   in
-    if (not !check) && not (occur_meta trm) then
+    if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
       let t'ty = Retyping.get_type_of env sigma trm in
       let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
         (goalacc,t'ty,sigma,trm)
@@ -346,7 +346,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       match kind_of_term trm with
       | Meta _ ->
 	let conclty = nf_betaiota sigma conclty in
-	  if !check && occur_meta conclty then
+	  if !check && occur_meta sigma (EConstr.of_constr conclty) then
 	    raise (RefinerError (MetaInType conclty));
 	  let (gl,ev,sigma) = mk_goal hyps conclty in
 	  gl::goalacc, conclty, sigma, ev
@@ -367,10 +367,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env f then
+	  if is_template_polymorphic env sigma (EConstr.of_constr f) then
 	    let ty = 
 	      (* Template sort-polymorphism of definition and inductive types *)
-	      let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
 	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
 	        type_of_global_reference_knowing_parameters env sigma f args
 	    in
@@ -406,7 +406,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	(acc'',conclty',sigma, ans)
 
       | _ ->
-	if occur_meta trm then
+	if occur_meta sigma (EConstr.of_constr trm) then
 	  anomaly (Pp.str "refiner called with a meta in non app/case subterm");
 	let t'ty = goal_type_of env sigma trm in
 	let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
@@ -432,9 +432,9 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env f
+	  if is_template_polymorphic env sigma (EConstr.of_constr f)
 	  then
-	    let l' = meta_free_prefix l in	      
+	    let l' = meta_free_prefix sigma l in
 	   (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f)
 	  else mk_hdgoals sigma goal goalacc f
 	in
@@ -464,7 +464,7 @@ and mk_hdgoals sigma goal goalacc trm =
 	   (acc',ty,sigma,c)
 
     | _ ->
-	if !check && occur_meta trm then
+	if !check && occur_meta sigma (EConstr.of_constr trm) then
 	  anomaly (Pp.str "refine called with a dependent meta");
 	goalacc, goal_type_of env sigma trm, sigma, trm
 
@@ -511,9 +511,9 @@ let convert_hyp check sign sigma d =
         if check && not (Option.equal (is_conv env sigma) b c) then
 	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the body of "++ pr_id id ++ str ".");
-       if check then reorder := check_decl_position env sign d;
+       if check then reorder := check_decl_position env sigma sign d;
        d) in
-  reorder_val_context env sign' !reorder
+  reorder_val_context env sigma sign' !reorder
 
 
 
@@ -537,7 +537,7 @@ let prim_refiner r sigma goal =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
 	    let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
-	    move_hyp false ([], LocalAssum (id,t),named_context_of_val sign)
+	    move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign)
 	      nexthyp,
 	      t,cl,sigma
 	  else
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0dba9ef1e..8c8a01cad 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -57,5 +57,5 @@ val catchable_exception : exn -> bool
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   Context.Named.Declaration.t -> Environ.named_context_val
 
-val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 34443b93d..a442a5e63 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -25,7 +25,7 @@ open Misctypes
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
   let ctyp = Retyping.get_type_of env sigma c in
-  if Termops.occur_meta_or_existential c then
+  if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then
     error "vm_compute does not support existential variables.";
   Vnorm.cbv_vm env c ctyp