diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-09 18:05:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-09 18:05:28 +0000 |
| commit | bd4034520da83bc667161c0e397b3720d3884b2f (patch) | |
| tree | 771434bfd7afd7d65b9d509f183c5fd457b816e3 /tactics | |
| parent | 148a1f26081f89cc6c2d17349b66a8de5074eca7 (diff) | |
Uniformization: isevars -> evdref/sigma/evd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16497 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 30daa03ea..5722c11ea 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 |