diff options
| author | ppedrot | 2012-06-22 15:14:30 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-22 15:14:30 +0000 |
| commit | 6b45f2d36929162cf92272bb60c2c245d9a0ead3 (patch) | |
| tree | 93aa975697b7de73563c84773d99b4c65b92173b /pretyping/unification.ml | |
| parent | fea214f82954197d23fda9a0e4e7d93e0cbf9b4c (diff) | |
Added an indirection with respect to Loc in Compat. As many [open Compat]
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4bf0928dce..27e5864b35 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -123,7 +123,7 @@ let pose_all_metas_as_evars env evd t = | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = if mvs = Evd.Metaset.empty then ty else aux ty in - let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in + let ev = Evarutil.e_new_evar evdref env ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; ev) | _ -> @@ -782,7 +782,7 @@ let applyHead env evd n c = match kind_of_term (whd_betadeltaiota env evd cty) with | Prod (_,c1,c2) -> let (evd',evar) = - Evarutil.new_evar evd env ~src:(dummy_loc,Evar_kinds.GoalEvar) c1 in + Evarutil.new_evar evd env ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in @@ -797,7 +797,7 @@ let is_mimick_head ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in + let (evd',j') = inh_conv_coerce_rigid_to Loc.ghost env evd j tycon in let evd' = Evarconv.consider_remaining_unif_problems env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) |