diff options
| author | barras | 2002-04-02 07:58:21 +0000 |
|---|---|---|
| committer | barras | 2002-04-02 07:58:21 +0000 |
| commit | 07686164a1279de0eff608f87ffe283dd34c1637 (patch) | |
| tree | 16ce941d8fbada87a7c2b778edea31dec4c565fa /tactics | |
| parent | 425f5dc5df05a85ddd35dd54136a94eb7baeb1f2 (diff) | |
- modifs de la condition de garde pour mieux tenir compte des raisonnements
par l'absurde
- un open_constr est maintenant un terme accompagne du sigma dans lequel il
est typable (il manquait l'info concernant le contexte de typage des
nouvelles evars)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/refine.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index ddddd21d88..a942b37b71 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -334,8 +334,9 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl = (* Et finalement la tactique refine elle-même : *) let refine oc gl = + let sigma = project gl in let env = pf_env gl in - let (gmm,c) = Clenv.exist_to_meta oc in + let (gmm,c) = Clenv.exist_to_meta sigma oc in let th = compute_metamap env gmm c in tcc_aux th gl |