diff options
| author | barras | 2004-09-15 16:50:56 +0000 |
|---|---|---|
| committer | barras | 2004-09-15 16:50:56 +0000 |
| commit | 2d707f4445c0cc86d8f8c30bdbe9eecf956997f9 (patch) | |
| tree | 9d6c2ff5489ba6bbf5683963108c34aa10b81e6f /tactics/equality.ml | |
| parent | 8f5a7bbf2e5c64d6badd9e7c39da83d07b9c6f40 (diff) | |
hiding the meta_map in evar_defs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index f9834f5229..8dcc8e06bb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -567,7 +567,7 @@ let minimal_free_rels env sigma (c,cty) = let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let { intro = exist_term } = find_sigma_data sort_of_ty in - let isevars = ref (Evarutil.create_evar_defs sigma) in + let isevars = ref (Evd.create_evar_defs sigma) in let rec sigrec_clausal_form siglen p_i = if siglen = 0 then if Evarconv.e_conv env isevars p_i dFLTty then @@ -579,19 +579,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let (a,p_i_minus_1) = match whd_beta_stack p_i with | (_sigS,[a;p]) -> (a,p) | _ -> anomaly "sig_clausal_form: should be a sigma type" in - let ev = Evarutil.e_new_isevar isevars env (dummy_loc,InternalHole) - (Evarutil.new_Type ()) in + let ev = Evarutil.e_new_evar isevars env (new_Type ()) in let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match - Evd.existential_opt_value (Evarutil.evars_of !isevars) + Evd.existential_opt_value (Evd.evars_of !isevars) (destEvar ev) with | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) | None -> anomaly "Not enough components to build the dependent tuple" in let scf = sigrec_clausal_form siglen ty in - Evarutil.nf_evar (Evarutil.evars_of !isevars) scf + Evarutil.nf_evar (Evd.evars_of !isevars) scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors |