diff options
| author | herbelin | 2007-05-29 10:01:06 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-29 10:01:06 +0000 |
| commit | 28a551e49864bbfee8a9212fdbcc364d1132b19e (patch) | |
| tree | af54777193da1f6e12e60e295006c13cf5247f34 /pretyping/clenv.ml | |
| parent | 7b00173a3e2cb44162e6d90e9306b20621ad046b (diff) | |
Correction d'un bug dans l'affichage du message d'erreur real_clean
(cas d'un terme sans Rel libre), introduction au passage d'un nouveau
type d'evar EvarGoal pour raffinement du message d'erreur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/clenv.ml')
| -rw-r--r-- | pretyping/clenv.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 5f4293abf1..1c35f9f720 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -132,7 +132,7 @@ let clenv_environments_evars env evd bound t = let clenv_conv_leq env sigma t c bound = let ty = Retyping.get_type_of env sigma c in - let evd = Evd.create_evar_defs sigma in + let evd = Evd.create_goal_evar_defs sigma in let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in let evars,_ = Evarconv.consider_remaining_unif_problems env evars in @@ -141,7 +141,7 @@ let clenv_conv_leq env sigma t c bound = args let mk_clenv_from_n gls n (c,cty) = - let evd = create_evar_defs gls.sigma in + let evd = create_goal_evar_defs gls.sigma in let (env,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); templtyp = mk_freelisted concl; @@ -263,7 +263,8 @@ let clenv_pose_dependent_evars clenv = List.fold_left (fun clenv mv -> let ty = clenv_meta_type clenv mv in - let (evd,evar) = new_evar clenv.evd (cl_env clenv) ty in + let (evd,evar) = + new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in clenv_assign mv evar {clenv with evd=evd}) clenv dep_mvs |