diff options
| author | herbelin | 2006-05-02 14:54:14 +0000 |
|---|---|---|
| committer | herbelin | 2006-05-02 14:54:14 +0000 |
| commit | ca2bca80347b0983e9a0b420360121ef82d72c71 (patch) | |
| tree | 3a81b21288e999285bd9e595ada182cfb09ec2e4 | |
| parent | 8a02b7d87eccf51893f13764841e833fae6079d1 (diff) | |
Correction bug du correctif bug assert as
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8778 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tactics.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0c05792959..0314c960ca 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1078,9 +1078,12 @@ let letin_tac with_eq name c occs gl = (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) let forward usetac ipat c gl = - let tac = match usetac with None -> exact_no_check c | Some tac -> tac in - let t = refresh_universes (pf_type_of gl c) in - tclTHENFIRST (assert_as true ipat t) tac gl + match usetac with + | None -> + let t = refresh_universes (pf_type_of gl c) in + tclTHENFIRST (assert_as true ipat t) (exact_no_check c) gl + | Some tac -> + tclTHENFIRST (assert_as true ipat c) tac gl (*****************************) (* High-level induction *) |