diff options
| author | narboux | 2003-11-12 18:03:50 +0000 |
|---|---|---|
| committer | narboux | 2003-11-12 18:03:50 +0000 |
| commit | ecf5fbd6bc5fc12166dd36c1b12ec714b86d0a63 (patch) | |
| tree | 2c9927b2d22c456dd07daddff5cc56cabdfb8b2d /toplevel | |
| parent | ea9f6b8f620b9f69de9d72ca603af042e4487339 (diff) | |
Idtac peut prendre un argument à afficher
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 541422261c..5edc4eaf8a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -580,8 +580,8 @@ let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = if not (refining ()) then error "Unknown command of the non proof-editing mode"; - if tac <> Tacexpr.TacId then set_end_tac (Tacinterp.interp tac) - + if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac) +(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) (*****************************) |