diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-15 16:50:56 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-15 16:50:56 +0000 |
| commit | 2d707f4445c0cc86d8f8c30bdbe9eecf956997f9 (patch) | |
| tree | 9d6c2ff5489ba6bbf5683963108c34aa10b81e6f /pretyping/evarconv.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 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6454e0e84..2ed26c92c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -19,6 +19,7 @@ open Classops open Recordops open Evarutil open Libnames +open Evd type flex_kind_of_term = | Rigid of constr @@ -175,13 +176,13 @@ let rec evar_conv_x env isevars pbty term1 term2 = (* Maybe convertible but since reducing can erase evars which [evar_apprec]*) (* could have found, we do it only if the terms are free of evar *) if - (not (has_undefined_isevars isevars term1) & - not (has_undefined_isevars isevars term2) & + (not (has_undefined_evars isevars term1) & + not (has_undefined_evars isevars term2) & is_fconv pbty env (evars_of isevars) term1 term2) then (isevars,true) - else if ise_undefined isevars term1 then + else if is_undefined_evar isevars term1 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) - else if ise_undefined isevars term2 then + else if is_undefined_evar isevars term2 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1) else let (t1,l1) = apprec_nohdbeta env isevars term1 in @@ -438,8 +439,8 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = let (isevars',ks) = List.fold_left (fun (i,ks) b -> - let dloc = (dummy_loc,Rawterm.InternalHole) in - let (i',ev) = new_isevar i env dloc (substl ks b) in + let dloc = (dummy_loc,InternalHole) in + let (i',ev) = new_evar i env ~src:dloc (substl ks b) in (i', ev :: ks)) (isevars,[]) bs in |