diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 17:14:02 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 17:14:02 +0000 |
| commit | 85fb5f33b1cac28e1fe4f00741c66f6f58109f84 (patch) | |
| tree | 4913998a925cb148c74a607bf7523ae1d28853ce /tactics/equality.ml | |
| parent | 31ebb89fe48efe92786b1cddc3ba62e7dfc4e739 (diff) | |
premiere reorganisation de l\'unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index a7e8c356e..bfedc8220 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -20,7 +20,6 @@ open Inductiveops open Environ open Libnames open Reductionops -open Instantiate open Typeops open Typing open Retyping @@ -585,7 +584,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match - Instantiate.existential_opt_value (Evarutil.evars_of isevars) + Evd.existential_opt_value (Evarutil.evars_of isevars) (destEvar ev) with | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) |