Uniformization: isevars -> evdref/sigma/evd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16497 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 87 insertions, 87 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 969fa7cbb6..d942ba0d04 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1860,7 +1860,7 @@ let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |])
 
 let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true))
 
-let constr_of_pat env isevars arsign pat avoid =
+let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
     match pat with
     | PatVar (l,name) ->
@@ -1875,9 +1875,9 @@ let constr_of_pat env isevars arsign pat avoid =
     | PatCstr (l,((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
 	let IndType (indf, _) = 
-	  try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty)
+	  try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
 	  with Not_found -> error_case_not_inductive env 
-	    {uj_val = ty; uj_type = Typing.type_of env !isevars ty}
+	    {uj_val = ty; uj_type = Typing.type_of env !evdref ty}
 	in
 	let ind, params = dest_ind_family indf in
 	if not (eq_ind ind cind) then error_bad_constructor_loc l cstr ind;
@@ -1903,8 +1903,8 @@ let constr_of_pat env isevars arsign pat avoid =
 	let cstr = mkConstruct ci.cs_cstr in
 	let app = applistc cstr (List.map (lift (List.length sign)) params) in
 	let app = applistc app args in
-	let apptype = Retyping.get_type_of env ( !isevars) app in
-	let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in
+	let apptype = Retyping.get_type_of env ( !evdref) app in
+	let IndType (indf, realargs) = find_rectype env ( !evdref) apptype in
 	  match alias with
 	      Anonymous ->
 		pat', sign, app, apptype, realargs, n, avoid
@@ -1914,8 +1914,8 @@ let constr_of_pat env isevars arsign pat avoid =
 		let sign, i, avoid =
 		  try
 		    let env = push_rel_context sign env in
-		    isevars := the_conv_x_leq (push_rel_context sign env)
-		      (lift (succ m) ty) (lift 1 apptype) !isevars;
+		    evdref := the_conv_x_leq (push_rel_context sign env)
+		      (lift (succ m) ty) (lift 1 apptype) !evdref;
 		    let eq_t = mk_eq (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
 		      (lift 1 app) (* aliased term *)
@@ -2018,7 +2018,7 @@ let build_ineqs prevpatterns pats liftsign =
   in match diffs with [] -> None
     | _ -> Some (mk_coq_and diffs)
 
-let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
+let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
   let i = ref 0 in
   let (x, y, z) =
     List.fold_left
@@ -2026,7 +2026,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	 let _, newpatterns, pats =
 	   List.fold_left2
 	     (fun (idents, newpatterns, pats) pat arsign ->
-		let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in
+		let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in
 		  (idents, pat' :: newpatterns, cpat :: pats))
 	      ([], [], []) eqn.patterns sign
 	 in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 70fc659cbc..fb5569e2e8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -65,11 +65,11 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
 
 open Program
 
-let make_existential loc ?(opaque = Evar_kinds.Define true) env isevars c =
-  Evarutil.e_new_evar isevars env ~src:(loc, Evar_kinds.QuestionMark opaque) c
+let make_existential loc ?(opaque = Evar_kinds.Define true) env evdref c =
+  Evarutil.e_new_evar evdref env ~src:(loc, Evar_kinds.QuestionMark opaque) c
 
-let app_opt env evars f t =
-  whd_betaiota !evars (app_opt f t)
+let app_opt env evdref f t =
+  whd_betaiota !evdref (app_opt f t)
 
 let pair_of_array a = (a.(0), a.(1))
 let make_name s = Name (Id.of_string s)
@@ -91,8 +91,8 @@ let disc_subset x =
 
 exception NoSubtacCoercion
   
-let hnf env isevars c = whd_betadeltaiota env isevars c
-let hnf_nodelta env evars c = whd_betaiota evars c
+let hnf env evd c = whd_betadeltaiota env evd c
+let hnf_nodelta env evd c = whd_betaiota evd c
 
 let lift_args n sign =
   let rec liftrec k = function
@@ -101,34 +101,34 @@ let lift_args n sign =
   in
     liftrec (List.length sign) sign
 
-let mu env isevars t =
+let mu env evdref t =
   let rec aux v =
-    let v' = hnf env !isevars v in
+    let v' = hnf env !evdref v in
       match disc_subset v' with
       Some (u, p) ->
 	let f, ct = aux u in
-	let p = hnf_nodelta env !isevars p in
+	let p = hnf_nodelta env !evdref p in
 	  (Some (fun x ->
-		   app_opt env isevars 
+		   app_opt env evdref 
 		     f (mkApp (delayed_force sig_proj1,
 			       [| u; p; x |]))),
 	   ct)
       | None -> (None, v)
   in aux t
 
-and coerce loc env isevars (x : Term.constr) (y : Term.constr)
+and coerce loc env evdref (x : Term.constr) (y : Term.constr)
     : (Term.constr -> Term.constr) option
     =
   let rec coerce_unify env x y =
-    let x = hnf env !isevars x and y = hnf env !isevars y in
+    let x = hnf env !evdref x and y = hnf env !evdref y in
       try
-	isevars := the_conv_x_leq env x y !isevars;
+	evdref := the_conv_x_leq env x y !evdref;
 	None
       with UnableToUnify _ -> coerce' env x y
   and coerce' env x y : (Term.constr -> Term.constr) option =
-    let subco () = subset_coerce env isevars x y in
+    let subco () = subset_coerce env evdref x y in
     let dest_prod c =
-      match Reductionops.splay_prod_n env ( !isevars) 1 c with
+      match Reductionops.splay_prod_n env ( !evdref) 1 c with
       | [(na,b,t)], c -> (na,t), c
       | _ -> raise NoSubtacCoercion
     in
@@ -137,7 +137,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
       let rec aux tele typ typ' i co =
 	if i < len then
 	  let hdx = l.(i) and hdy = l'.(i) in
-	    try isevars := the_conv_x_leq env hdx hdy !isevars;
+	    try evdref := the_conv_x_leq env hdx hdy !evdref;
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
 		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
@@ -145,7 +145,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
 	      let _ =
-		try isevars := the_conv_x_leq env eqT eqT' !isevars
+		try evdref := the_conv_x_leq env eqT eqT' !evdref
 		with UnableToUnify _ -> raise NoSubtacCoercion
 	      in
 		(* Disallow equalities on arities *)
@@ -156,7 +156,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
 		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
 		let eq = mkApp (delayed_force coq_eq_ind, [| eqT; hdx; hdy |]) in
-		let evar = make_existential loc env isevars eq in
+		let evar = make_existential loc env evdref eq in
 		let eq_app x = mkApp (delayed_force coq_eq_rect,
 				      [| eqT; hdx; pred; x; hdy; evar|]) in
 		  aux (hdy :: tele) (subst1 hdx restT) 
@@ -180,7 +180,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	  let env' = push_rel (name', None, a') env in
 	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 	    (* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
-	  let coec1 = app_opt env' isevars c1 (mkRel 1) in
+	  let coec1 = app_opt env' evdref c1 (mkRel 1) in
 	    (* env, x : a' |- c1[x] : lift 1 a *)
 	  let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
 	    (* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
@@ -190,7 +190,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		 Some
 		   (fun f ->
 		      mkLambda (name', a',
-				app_opt env' isevars c2
+				app_opt env' evdref c2
 				  (mkApp (lift 1 f, [| coec1 |])))))
 
       | App (c, l), App (c', l') ->
@@ -215,13 +215,13 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		       | Lambda (n, t, t') -> c, t'
 			   (*| Prod (n, t, t') -> t'*)
 		       | Evar (k, args) ->
-			   let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in
-			     isevars := evs;
+			   let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in
+			     evdref := evs;
 			     let (n, dom, rng) = destLambda t in
-			     let dom = whd_evar !isevars dom in
+			     let dom = whd_evar !evdref dom in
 			       if isEvar dom then
 				 let (domk, args) = destEvar dom in
-				   isevars := define domk a !isevars;
+				   evdref := define domk a !evdref;
 			       else ();
 			       t, rng
 		       | _ -> raise NoSubtacCoercion
@@ -235,9 +235,9 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 			   Some
 			     (fun x ->
 				let x, y =
-				  app_opt env' isevars c1 (mkApp (delayed_force sigT_proj1,
+				  app_opt env' evdref c1 (mkApp (delayed_force sigT_proj1,
 								  [| a; pb; x |])),
-				  app_opt env' isevars c2 (mkApp (delayed_force sigT_proj2,
+				  app_opt env' evdref c2 (mkApp (delayed_force sigT_proj2,
 								  [| a; pb; x |]))
 				in
 				  mkApp (delayed_force sigT_intro, [| a'; pb'; x ; y |]))
@@ -255,16 +255,16 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 			   Some
 			     (fun x ->
 				let x, y =
-				  app_opt env isevars c1 (mkApp (delayed_force prod_proj1,
+				  app_opt env evdref c1 (mkApp (delayed_force prod_proj1,
 								 [| a; b; x |])),
-				  app_opt env isevars c2 (mkApp (delayed_force prod_proj2,
+				  app_opt env evdref c2 (mkApp (delayed_force prod_proj2,
 								 [| a; b; x |]))
 				in
 				  mkApp (delayed_force prod_intro, [| a'; b'; x ; y |]))
 		   end
 	       else
 		 if eq_ind i i' && Int.equal len (Array.length l') then
-		   let evm = !isevars in
+		   let evm = !evdref in
 		     (try subco ()
 		      with NoSubtacCoercion ->
 			let typ = Typing.type_of env evm c in
@@ -276,7 +276,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		   subco ()
 	   | x, y when Pervasives.(=) x y -> (** FIXME *)
 	       if Int.equal (Array.length l) (Array.length l') then
-		 let evm =  !isevars in
+		 let evm =  !evdref in
 		 let lam_type = Typing.type_of env evm c in
 		 let lam_type' = Typing.type_of env evm c' in
 		   (* 			 if not (is_arity env evm lam_type) then ( *)
@@ -286,12 +286,12 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	   | _ -> subco ())
       | _, _ ->  subco ()
 
-  and subset_coerce env isevars x y =
+  and subset_coerce env evdref x y =
     match disc_subset x with
     Some (u, p) ->
       let c = coerce_unify env u y in
       let f x =
-	app_opt env isevars c (mkApp (delayed_force sig_proj1,
+	app_opt env evdref c (mkApp (delayed_force sig_proj1,
 				      [| u; p; x |]))
       in Some f
     | None ->
@@ -300,23 +300,23 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	  let c = coerce_unify env x u in
 	    Some
 	      (fun x ->
-		 let cx = app_opt env isevars c x in
-		 let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
+		 let cx = app_opt env evdref c x in
+		 let evar = make_existential loc env evdref (mkApp (p, [| cx |]))
 		 in
 		   (mkApp
 		      (delayed_force sig_intro,
 		       [| u; p; cx; evar |])))
 	| None ->
 	    raise NoSubtacCoercion
-	      (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars;
+	      (*evdref := Evd.add_conv_pb (Reduction.CONV, x, y) !evdref;
 		None*)
   in coerce_unify env x y
 
-let coerce_itf loc env isevars v t c1 =
-  let evars = ref isevars in
-  let coercion = coerce loc env evars t c1 in
-  let t = Option.map (app_opt env evars coercion) v in
-    !evars, t
+let coerce_itf loc env evd v t c1 =
+  let evdref = ref evd in
+  let coercion = coerce loc env evdref t c1 in
+  let t = Option.map (app_opt env evdref coercion) v in
+    !evdref, t
 
 let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
@@ -351,10 +351,10 @@ let inh_app_fun env evd j =
 	  (evd,apply_coercion env evd p j t)
 	with Not_found when Flags.is_program_mode () ->
 	  try
-	    let isevars = ref evd in
-	    let coercef, t = mu env isevars t in
-	    let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in
-	      (!isevars, res)
+	    let evdref = ref evd in
+	    let coercef, t = mu env evdref t in
+	    let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
+	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
 
@@ -385,19 +385,19 @@ let inh_coerce_to_sort loc env evd j =
 
 let inh_coerce_to_base loc env evd j =
   if Flags.is_program_mode () then
-    let isevars = ref evd in
-    let ct, typ' = mu env isevars j.uj_type in
+    let evdref = ref evd in
+    let ct, typ' = mu env evdref j.uj_type in
     let res =
-      { uj_val = app_opt env isevars ct j.uj_val;
+      { uj_val = app_opt env evdref ct j.uj_val;
 	uj_type = typ' }
-    in !isevars, res
+    in !evdref, res
   else (evd, j)
 
 let inh_coerce_to_prod loc env evd t =
   if Flags.is_program_mode () then
-    let isevars = ref evd in
-    let _, typ' = mu env isevars t in
-      !isevars, typ'
+    let evdref = ref evd in
+    let _, typ' = mu env evdref t in
+      !evdref, typ'
   else (evd, t)
 
 let inh_coerce_to_fail env evd rigidonly v t c1 =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 30daa03ea2..5722c11eae 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1776,7 +1776,7 @@ let build_morphism_signature m =
   let env = Global.env () in
   let m = Constrintern.interp_constr Evd.empty env m in
   let t = Typing.type_of env Evd.empty m in
-  let isevars = ref (Evd.empty, Evd.empty) in
+  let evdref = ref (Evd.empty, Evd.empty) in
   let cstrs =
     let rec aux t =
       match kind_of_term t with
@@ -1785,21 +1785,21 @@ let build_morphism_signature m =
 	| _ -> []
     in aux t
   in
-  let evars, t', sig_, cstrs = build_signature !isevars env t cstrs None in
-  let _ = isevars := evars in
+  let evars, t', sig_, cstrs = build_signature !evdref env t cstrs None in
+  let _ = evdref := evars in
   let _ = List.iter
     (fun (ty, rel) ->
       Option.iter (fun rel ->
 	let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
-	let evars,c = new_cstr_evar !isevars env default in
-	  isevars := evars)
+	let evars,c = new_cstr_evar !evdref env default in
+	  evdref := evars)
 	rel)
     cstrs
   in
   let morph =
     mkApp (Lazy.force proper_type, [| t; sig_; m |])
   in
-  let evd = solve_constraints env !isevars in
+  let evd = solve_constraints env !evdref in
   let m = Evarutil.nf_evar evd morph in
     Evarutil.check_evars env Evd.empty evd m; m
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 47d4965285..85c67a5c7a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -615,27 +615,27 @@ let rec telescope = function
   | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in
       ty, ((n, Some b, t) :: subst), lift 1 term
 
-let nf_evar_context isevars ctx =
+let nf_evar_context sigma ctx =
   List.map (fun (n, b, t) ->
-    (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx
+    (n, Option.map (Evarutil.nf_evar sigma) b, Evarutil.nf_evar sigma t)) ctx
 
 let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let sigma = Evd.empty in
-  let isevars = ref (Evd.create_evar_defs sigma) in
+  let evdref = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in
-  let _, ((env', binders_rel), impls) = interp_context_evars isevars env bl in
+  let _, ((env', binders_rel), impls) = interp_context_evars evdref env bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
-  let top_arity = interp_type_evars isevars top_env arityc in
+  let top_arity = interp_type_evars evdref top_env arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let argtyp, letbinders, make = telescope binders_rel in
   let argname = Id.of_string "recarg" in
   let arg = (Name argname, None, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
-  let rel, _ = interp_constr_evars_impls ~evdref:isevars env r in
-  let relty = Typing.type_of env !isevars rel in
+  let rel, _ = interp_constr_evars_impls ~evdref env r in
+  let relty = Typing.type_of env !evdref rel in
   let relargty =
     let error () =
       user_err_loc (constr_loc r,
@@ -643,14 +643,14 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 		    Printer.pr_constr_env env rel ++ str " is not an homogeneous binary relation.")
     in
       try
-	let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
+	let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
 	  match ctx, kind_of_term ar with
 	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
-	      when Reductionops.is_conv env !isevars t u -> t
+	      when Reductionops.is_conv env !evdref t u -> t
 	  | _, _ -> error ()
       with e when Errors.noncritical e -> error ()
   in
-  let measure = interp_casted_constr_evars isevars binders_env measure relargty in
+  let measure = interp_casted_constr_evars evdref binders_env measure relargty in
   let wf_rel, wf_rel_fun, measure_fn =
     let measure_body, measure =
       it_mkLambda_or_LetIn measure letbinders,
@@ -703,7 +703,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     let newimpls = Id.Map.singleton recname
       (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
        scopes @ [None]) in
-      interp_casted_constr_evars isevars ~impls:newimpls
+      interp_casted_constr_evars evdref ~impls:newimpls
 	(push_rel_context ctx env) body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
@@ -711,14 +711,14 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let def =
     mkApp (constr_of_global (delayed_force fix_sub_ref),
 	  [| argtyp ; wf_rel ;
-	     Evarutil.e_new_evar isevars env 
+	     Evarutil.e_new_evar evdref env 
 	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop ; intern_body_lam |])
   in
-  let _ = isevars := Evarutil.nf_evar_map !isevars in
-  let binders_rel = nf_evar_context !isevars binders_rel in
-  let binders = nf_evar_context !isevars binders in
-  let top_arity = Evarutil.nf_evar !isevars top_arity in
+  let _ = evdref := Evarutil.nf_evar_map !evdref in
+  let binders_rel = nf_evar_context !evdref binders_rel in
+  let binders = nf_evar_context !evdref binders in
+  let top_arity = Evarutil.nf_evar !evdref top_arity in
   let hook, recname, typ = 
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
@@ -726,7 +726,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let ce =
-          { const_entry_body = Evarutil.nf_evar !isevars body;
+          { const_entry_body = Evarutil.nf_evar !evdref body;
             const_entry_secctx = None;
 	    const_entry_type = Some ty;
         const_entry_opaque = false;
@@ -747,11 +747,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
   in
-  let fullcoqc = Evarutil.nf_evar !isevars def in
-  let fullctyp = Evarutil.nf_evar !isevars typ in
-  Obligations.check_evars env !isevars;
+  let fullcoqc = Evarutil.nf_evar !evdref def in
+  let fullctyp = Evarutil.nf_evar !evdref typ in
+  Obligations.check_evars env !evdref;
   let evars, _, evars_def, evars_typ = 
-    Obligations.eterm_obligations env recname !isevars 0 fullcoqc fullctyp 
+    Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
     ignore(Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook)