Clarification changements autour de Remark/Fact/Local

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@3180 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 46 insertions, 26 deletions

diff --git a/CHANGES b/CHANGES
index b83c9adc11..eb0738d116 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,12 +19,16 @@ Language
 - Idem for assumptions declarations and constants when the type is mentionned.
 - The "Coercion" and "Canonical Structure" keywords now accept the
   same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t".
-- Remark and Fact now definitively behaves as Theorem and Lemma; when
-  sections are closed, the full names of Remark and Fact has no longer a
-  section part; Local built by tactics are now Opaque if the proof is
-  ended by Qed.
-- Opaque local statements (such as defined by Local ... Qed, see above) have
-  their body hidden in the local context of proofs
+- Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u".
+- Remark's and Fact's now definitively behave as Theorem and Lemma: when
+  sections are closed, the full name of a Remark or a Fact has no longer a
+  section part (source of incompatibilities)
+- Opaque Local's (i.e. built by tactics and ended by Qed), do not
+  survive section closing any longer; as a side-effect, Opaque Local's
+  now appear in the local context of proofs; their body is hidden
+  though (source of incompatibilities); use one of Remark/Fact/Lemma/Theorem
+  instead to simulate the old behaviour of Local (the section part of
+  the name is not kept though)
 
 ML tactic and vernacular commands
 
@@ -69,6 +73,12 @@ Incompatibilities
 - Transparency of le_lt_dec and co (leads to some simplification in
   proofs; in some cases, incompatibilites is solved by declaring locally 
   opaque the relevant constant)
+- Opaque Local do not now survive section closing (rename them into
+  Remark/Lemma/... to get them still surviving the sections; this
+  renaming allows also to solve incompatibilites related to now
+  forbidden calls to the tactic Clear)
+- Remark and Fact have no longer (very) long names (use Local instead in case
+  of name conflict)
 
 Bugs
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ef7539bffd..7142f1e6d1 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1782,9 +1782,11 @@ let xlate_vernac =
   | VernacBeginSection id ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment id -> CT_section_end (xlate_ident id)
-  | VernacStartTheoremProof (k, s, c, _, _) ->
+  | VernacStartTheoremProof (k, s, ([],c), _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,xlate_constr c))
+  | VernacStartTheoremProof (k, s, (bl,c), _, _) -> 
+      xlate_error "TODO: VernacStartTheoremProof"
   | VernacSuspend -> CT_suspend
   | VernacResume idopt -> CT_resume (xlate_ident_opt idopt)
   | VernacDefinition (k,s,ProveBody (bl,typ),_) ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 146bce48df..c3afc0956c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -173,8 +173,8 @@ ident_comma_list_tail:
   ;
   gallina:
     (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = ident; ":"; c = constr -> 
-         VernacStartTheoremProof (thm, id, c, false, (fun _ _ -> ()))
+    [ [ thm = thm_token; id = ident; bl = binders_list; ":"; c = constr ->
+         VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
       | (f,d) = def_token; id = ident; b = def_body -> 
           VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = ne_params_list -> 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a670c2bda2..fd2041d31b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -468,7 +468,19 @@ let build_scheme lnamedepindsort =
   let lrecref = List.fold_right2 declare listdecl lrecnames [] in
   if_verbose ppnl (recursive_message (Array.of_list lrecref))
 
-let start_proof_com sopt (local,stre) com hook =
+let rec generalize_rawconstr c = function
+  | [] -> c
+  | LocalRawDef (id,b)::bl -> Ast.mkLetInC(id,b,generalize_rawconstr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> Ast.mkProdC(x,t,b)) idl
+        (generalize_rawconstr c bl)
+
+let rec binders_length = function
+  | [] -> 0
+  | LocalRawDef _::bl -> 1 + binders_length bl
+  | LocalRawAssum (idl,_)::bl -> List.length idl + binders_length bl
+
+let start_proof_com sopt (local,stre) (bl,t) hook =
   let env = Global.env () in
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
@@ -482,7 +494,7 @@ let start_proof_com sopt (local,stre) com hook =
 	next_ident_away (id_of_string "Unnamed_thm")
 	  (Pfedit.get_all_proof_names ())
   in
-  let c = interp_type Evd.empty env com in
+  let c = interp_type Evd.empty env (generalize_rawconstr t bl) in
   let _ = Typeops.infer_type env c in
   Pfedit.start_proof id (local,stre) sign c hook
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 23c0db5b4d..88da5394a4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -47,7 +47,10 @@ val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
 
 val build_scheme : (identifier * bool * qualid located * Coqast.t) list -> unit
 
-val start_proof_com : identifier option -> bool * strength -> Coqast.t -> Proof_type.declaration_hook -> unit
+val generalize_rawconstr : Coqast.t -> local_binder list -> Coqast.t
+
+val start_proof_com : identifier option -> bool * strength -> 
+  (local_binder list * Coqast.t) -> Proof_type.declaration_hook -> unit
 
 (*s [save_named b] saves the current completed proof under the name it
 was started; boolean [b] tells if the theorem is declared opaque; it
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 49aae75bb6..d9baaa79c2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -334,13 +334,6 @@ let start_proof_and_print idopt k t hook =
   print_subgoals ();
   if !pcoq <> None then (out_some !pcoq).start_proof ()
 
-let rec generalize_rawconstr c = function
-  | [] -> c
-  | LocalRawDef (id,b)::bl -> Ast.mkLetInC(id,b,generalize_rawconstr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> Ast.mkProdC(x,t,b)) idl
-        (generalize_rawconstr c bl)
-
 let vernac_definition kind id def hook =
   let (local,stre as k) = interp_definition kind in
   match def with
@@ -350,8 +343,7 @@ let vernac_definition kind id def hook =
 	hook stre ref
       else
 	let hook _ _ = () in
-	let t = generalize_rawconstr t bl in
-	start_proof_and_print (Some id) k t hook
+	start_proof_and_print (Some id) k (bl,t) hook
   | DefineBody (bl,red_option,c,typ_opt) ->
       let red_option = match red_option with
         | None -> None
@@ -361,7 +353,7 @@ let vernac_definition kind id def hook =
       let ref = declare_definition id k bl red_option c typ_opt in
       hook stre ref
 
-let vernac_start_proof kind sopt t lettop hook =
+let vernac_start_proof kind sopt (bl,t) lettop hook =
   if not(refining ()) then
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
@@ -369,12 +361,13 @@ let vernac_start_proof kind sopt t lettop hook =
   let stre = interp_theorem kind in
   match Lib.is_specification (), sopt with
     | true, Some id ->
+        let t = generalize_rawconstr t bl in
 	let ref = declare_assumption id stre [] t in
 	hook stre ref
     | _ -> 
 	(* an explicit Goal command starts the refining mode 
 	   even in a specification *)
-	start_proof_and_print sopt (false, stre) t hook
+	start_proof_and_print sopt (false, stre) (bl,t) hook
 
 let vernac_end_proof is_opaque idopt =
   if_verbose show_script ();
@@ -1113,7 +1106,7 @@ let interp c = match c with
   | VernacNop -> ()
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof Theorem None t false (fun _ _ -> ())
+  | VernacGoal t -> vernac_start_proof Theorem None ([],t) false (fun _ _ ->())
   | VernacAbort id -> vernac_abort id
   | VernacAbortAll -> vernac_abort_all ()
   | VernacRestart -> vernac_restart ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 7ea61dd6e5..d7091bfa24 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -201,8 +201,8 @@ type vernac_expr =
   (* Gallina *)
   | VernacDefinition of definition_kind * identifier * definition_expr *
       Proof_type.declaration_hook
-  | VernacStartTheoremProof of theorem_kind * identifier * Coqast.t * bool *
-      Proof_type.declaration_hook
+  | VernacStartTheoremProof of theorem_kind * identifier *
+      (local_binder list * Coqast.t) * bool * Proof_type.declaration_hook
   | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
   | VernacExactProof of constr_ast
   | VernacAssumption of assumption_kind * simple_binder with_coercion list