diff options
| author | herbelin | 2002-10-23 23:01:37 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-23 23:01:37 +0000 |
| commit | 85c65e07e70e7001b3048ea01c40b052da42293c (patch) | |
| tree | 208544fabab99ff634f2395c87a6c1b66470a48b | |
| parent | e50635edb2504712ae9b88951e155549adfc5d04 (diff) | |
Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3179 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index a88906445f..8c2077f46c 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -415,7 +415,8 @@ let new_morphism m id hook = let lem = (gen_compat_lemma env m body args_t poss) in let lemast = (ast_of_constr true env lem) in new_edited id m poss; - start_proof_com (Some id) (false,Libnames.NeverDischarge) lemast hook; + start_proof_com (Some id) (false,Libnames.NeverDischarge) + ([],lemast) hook; (Options.if_verbose Vernacentries.show_open_subgoals ())) let rec sub_bool l1 n = function |