diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 21:40:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 21:40:03 +0000 |
| commit | c514fdd2ee105fcb5f471d123ed24c478fb27bed (patch) | |
| tree | b14cf0c4636f9f2a9523c9fb11d196ff0004cc81 /tactics | |
| parent | 44cafc5d7e5de836c096573f709f2465723240dc (diff) | |
Garder les cast semble décidément le meilleur moyen de rester synchrone avec l'environnement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6424 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/refine.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index 7f69a9c95..169e51467 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -133,15 +133,13 @@ let rec compute_metamap env c = match kind_of_term c with | (Const _ | Evar _ | Ind _ | Construct _ | Sort _ | Var _ | Rel _) -> TH (c,[],[]) + (* le terme est une mv => un but *) | Meta n -> - (* - Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n); - let ty = Retyping.get_type_of_with_meta env Evd.empty lmeta c in - *) TH (c,[],[None]) + | Cast (m,ty) when isMeta m -> - TH (m,[destMeta m,ty],[None]) + TH (c,[destMeta m,ty],[None]) (* abstraction => il faut décomposer si le terme dessous n'est pas pur * attention : dans ce cas il faut remplacer (Rel 1) par (Var x) @@ -351,11 +349,9 @@ let coerce_to_goal (sigma,c) gl = let refine oc gl = let sigma = project gl in - let env = pf_env gl in let oc = coerce_to_goal oc gl in let (_gmm,c) = Evarutil.exist_to_meta sigma oc in (* Relies on Cast's put on Meta's by exist_to_meta, because it is otherwise complicated to update gmm when passing through a binder *) - let th = compute_metamap env c in + let th = compute_metamap (pf_env gl) c in tcc_aux [] th gl - |