Ajout du Let pour le langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 288 insertions, 48 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 4aa22a71b3..a653b1c046 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -77,7 +77,8 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
    match tag with
       "CONSTANT" ->
         (match D.constant_strength sp with
-            D.DischargeAt _  -> false (* a local definition *)
+          | D.DischargeAt _  -> false (* a local definition *)
+          | D.NotDeclare     -> false (* not a definition *)
           | D.NeverDischarge -> true  (* a non-local one    *)
         )
     | "PARAMETER"                 (* axioms and                               *)
diff --git a/library/declare.ml b/library/declare.ml
index 621666d677..123cbd188f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -17,6 +17,7 @@ open Impargs
 open Indrec
 
 type strength = 
+  | NotDeclare
   | DischargeAt of dir_path
   | NeverDischarge
 
diff --git a/library/declare.mli b/library/declare.mli
index 3c5e996089..b902be207b 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -16,7 +16,8 @@ open Inductive
    reset works properly --- and will fill some global tables such as 
    [Nametab] and [Impargs]. *)
 
-type strength = 
+type strength =
+  | NotDeclare
   | DischargeAt of dir_path
   | NeverDischarge
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 0f0d70f8b3..1cd140ed64 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -33,15 +33,17 @@ GEXTEND Gram
     [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
       | IDENT "Goal"; "." -> <:ast< (GOAL) >>
       | "Proof"; "." -> <:ast< (GOAL) >>
+      |	IDENT "Begin"; "." -> <:ast< (GOAL) >>
       | IDENT "Abort"; "." -> <:ast< (ABORT) >>
       | "Qed"; "." -> <:ast< (SaveNamed) >>
       | IDENT "Save"; "." -> <:ast< (SaveNamed) >>
       | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
+      |	IDENT "Defined"; id = identarg; "." -> <:ast< (DefinedAnonymous $id) >>
       | IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
           <:ast< (SaveAnonymousRmk $id) >>
       | IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
           <:ast< (SaveAnonymousThm $id) >>
-      | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >>
+      | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymous $id) >>
       | IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
       | IDENT "Resume"; "." -> <:ast< (RESUME) >>
       | IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 99e7e136e5..18a9da82b3 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -212,7 +212,19 @@ GEXTEND Gram
       | "()" -> <:ast< (VOID) >> ] ]
   ;
   let_clause:
-    [ [ id = identarg; "="; te=tactic_expr -> <:ast< (LETCLAUSE $id $te) >> ] ]
+    [ [ id = identarg; "="; te=tactic_expr -> <:ast< (LETCLAUSE $id $te) >>
+      | id = identarg; ":"; c = constrarg; ":="; "Proof" ->
+        (match c with
+        | Coqast.Node(_,"COMMAND",[csr]) ->
+          <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
+	| _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">])
+      | id = identarg; ":"; c = constrarg; ":="; te = tactic_expr ->
+        <:ast< (LETCUTCLAUSE $id $c $te) >> 
+      |	id = identarg; ":"; c = constrarg ->
+        (match c with
+        | Coqast.Node(_,"COMMAND",[csr]) ->
+          <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
+	| _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">]) ] ]
   ;
   rec_clause:
     [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_expr ->
@@ -273,6 +285,17 @@ GEXTEND Gram
             <:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >>
       | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And"; IDENT "In";
           u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >>
+      |	IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And" ->
+        (match llc with
+	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
+          <:ast< (StartProof "LETTOP" $id $c) >>
+        | _ -> <:ast< (LETCUT (LETDECL ($LIST $llc))) >>)
+      |	IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And";
+        tb = Vernac.theorem_body; "Qed" ->
+        (match llc with
+	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
+          <:ast< (TheoremProof "LETTOP" $id $c $tb) >>
+	| _ -> errorlabstrm "Gram.tactic_atom" [<'sTR "Not a LETTOPCLAUSE">])
       |	IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
         -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
       |	IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list ->
@@ -308,7 +331,7 @@ GEXTEND Gram
       | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >>
       |	IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
         <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
-      |	"'"; c = ident_or_constrarg -> c ] ]
+      |	"'"; c = constrarg -> c ] ]
   ;
   simple_tactic:
     [ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2eab116658..7f22ba49af 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -22,7 +22,11 @@ GEXTEND Gram
       | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ]
   ;
   vernac: LAST
-    [ [ tac = tacarg; "." -> <:ast< (SOLVE 1 (TACTIC $tac)) >> ] ]
+    [ [ tac = tacarg; "." ->
+        (match tac with
+	| Coqast.Node(_,kind,_)
+          when kind = "StartProof" || kind = "TheoremProof" -> tac
+	| _ -> <:ast< (SOLVE 1 (TACTIC $tac)) >>) ] ]
   ;
   vernac_list_tail:
     [ [ v = vernac; l = vernac_list_tail -> v :: l
@@ -52,7 +56,8 @@ GEXTEND Gram
     [ [ "Theorem" -> <:ast< "THEOREM" >>
       | IDENT "Lemma" -> <:ast< "LEMMA" >>
       | IDENT "Fact" -> <:ast< "FACT" >>
-      | IDENT "Remark" -> <:ast< "REMARK" >> ] ]
+      | IDENT "Remark" -> <:ast< "REMARK" >>
+      | IDENT "Decl" -> <:ast< "DECL" >> ] ]
   ;
   def_tok:
     [ [ "Definition" -> <:ast< "DEFINITION" >>
@@ -103,7 +108,6 @@ GEXTEND Gram
       | thm = thm_tok; id = identarg; ":"; c = constrarg; ":="; "Proof";
         tb = theorem_body; "Qed"; "." ->
           <:ast< (TheoremProof $thm $id $c $tb) >>
-
       | def = def_tok; s = identarg; bl = binders_list;
 	":"; t = Constr.constr; "." ->
           <:ast< (StartProof $def $s (CONSTR ($ABSTRACT "PRODLIST" $bl $t))) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b109218177..5df722f1bb 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -289,6 +289,7 @@ module Tactic =
     let input_fun = gec "input_fun"
     let lconstrarg = gec "lconstrarg"
     let let_clause = gec "let_clause"
+    let letcut_clause = gec "letcut_clause"
     let clausearg = gec "clausearg"
     let match_context_rule = gec "match_context_rule"
     let match_hyps = gec "match_hyps"
@@ -360,6 +361,7 @@ module Vernac =
     let ne_constrarg_list = gec_list "ne_constrarg_list"
     let tacarg = gec "tacarg"
     let sortarg = gec "sortarg"
+    let theorem_body = gec "theorem_body"
 
     let gallina = gec "gallina"
     let gallina_ext = gec "gallina_ext"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c4f61aa75d..1999733f0e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -120,6 +120,7 @@ module Tactic :
     val lconstrarg : Coqast.t Gram.Entry.e
     val lconstrarg_binding_list : Coqast.t list Gram.Entry.e
     val let_clause : Coqast.t Gram.Entry.e
+    val letcut_clause : Coqast.t Gram.Entry.e
     val match_context_rule : Coqast.t Gram.Entry.e
     val match_hyps : Coqast.t Gram.Entry.e
     val match_pattern : Coqast.t Gram.Entry.e
@@ -172,6 +173,7 @@ module Vernac :
     val ne_constrarg_list : Coqast.t list Gram.Entry.e
     val tacarg : Coqast.t Gram.Entry.e
     val sortarg : Coqast.t Gram.Entry.e
+    val theorem_body : Coqast.t Gram.Entry.e
 
     val gallina : Coqast.t Gram.Entry.e
     val gallina_ext : Coqast.t Gram.Entry.e
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 33c5f862ee..007a2e4abc 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -434,7 +434,8 @@ let inspect depth =
 
 open Classops
 
-let string_of_strength = function 
+let string_of_strength = function
+  | NotDeclare -> "(temp)"
   | NeverDischarge -> "(global)"
   | DischargeAt sp -> "(disch@"^(string_of_dirpath sp)
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index e2f609072a..dd0199c0f0 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -3,6 +3,7 @@
 
 open Astterm
 open Closure
+open Declarations
 open Dyn
 open Libobject
 open Pattern
@@ -12,6 +13,7 @@ open Sign
 open Tacred
 open Util
 open Names
+open Pfedit
 open Proof_type
 open Tacmach
 open Tactic_debug
@@ -34,11 +36,22 @@ type value =
   | VVoid
   | VRec of value ref
 
+(* For tactic_of_value *)
+exception NotTactic
+
+(* Gives the tactic corresponding to the tactic value *)
+let tactic_of_value vle g =
+  match vle with
+  | VTactic tac -> (tac g)
+  | VFTactic (largs,f) -> (f largs g) 
+  | VRTactic res -> res
+  | _ -> raise NotTactic
+
 (* Gives the identifier corresponding to an Identifier tactic_arg *)
 let id_of_Identifier = function
   | Identifier id -> id
   | _ ->
-    anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">]
+    anomalylabstrm "id_of_Identifier" [<'sTR "Not an IDENTIFIER tactic_arg">]
 
 (* Gives the constr corresponding to a Constr tactic_arg *)
 let constr_of_Constr = function
@@ -55,15 +68,27 @@ let constr_of_Constr_context = function
 (* Transforms a named_context into a (string * constr) list *)
 let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ))
 
-(*  let lid = List.map string_of_id (ids_of_named_context hyps)
-  and lhyp = List.map body_of_type (vals_of_sign hyps) in
-    List.rev (List.combine lid lhyp)*)
+(* Transforms an id into a constr if possible *)
+let constr_of_id id = function
+  | None -> raise Not_found
+  | Some goal ->
+    let hyps = pf_hyps goal in
+    if mem_named_context id hyps then
+      mkVar id
+    else
+      let csr = Declare.global_reference CCI id in
+      (match kind_of_term csr with
+      | IsVar _ -> raise Not_found
+      | _ -> csr)
 
 (* Extracted the constr list from lfun *)
 let rec constr_list goalopt = function
   | (str,VArg(Constr c))::tl -> (id_of_string str,c)::(constr_list goalopt tl)
   | (str,VArg(Identifier id))::tl ->
-    (match goalopt with
+    (try (id_of_string str,(constr_of_id id goalopt))::(constr_list goalopt tl)
+     with | Not_found -> (constr_list goalopt tl))
+
+(*    (match goalopt with
     | None -> constr_list goalopt tl
     | Some goal ->
       let hyps = pf_hyps goal in
@@ -76,7 +101,7 @@ let rec constr_list goalopt = function
            | IsVar _ -> constr_list goalopt tl
   	   | _ -> (id_of_string str,csr)::(constr_list goalopt tl))
          with
-	 | Not_found -> (constr_list goalopt tl)))
+	 | Not_found -> (constr_list goalopt tl)))*)
 
 (*      (try
          let csr = Declare.global_reference CCI id in
@@ -425,8 +450,10 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
     | Node(_,"REC",l) ->
       rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast l
     | Node(_,"LET",[Node(_,"LETDECL",l);u]) ->
-      let addlfun=let_interp (evc,env,lfun,lmatch,goalopt,debug) ast l in
+      let addlfun=letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast l in
         val_interp (evc,env,(lfun@addlfun),lmatch,goalopt,debug) u
+    | Node(_,"LETCUT",[Node(_,"LETDECL",l)]) ->
+      VTactic (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast l)
     | Node(_,"MATCHCONTEXT",lmr) ->
       match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr
     | Node(_,"MATCH",lmr) ->
@@ -455,20 +482,18 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
       val_interp (evc,env,lfun,lmatch,goalopt,debug)
         (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))
     | Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) ->
-      VFTactic ([],(interp_atomic loc opn))
+      VFTactic ([],(interp_atomic opn))
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
       (try (unrec (List.assoc s lfun))
        with | Not_found ->
          (try (lookup s)
           with | Not_found -> VArg (Identifier (id_of_string s))))
-
     | Node(_,"QUALID",[Nvar(_,s)]) ->
       (try (unrec (List.assoc s lfun))
        with | Not_found ->
          (try (lookup s)
           with | Not_found -> VArg (Identifier (id_of_string s))))
-
     | Str(_,s) -> VArg (Quoted_string s)
     | Num(_,n) -> VArg (Integer n)
     | Node(_,"COMMAND",[c]) ->
@@ -564,7 +589,7 @@ and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
     anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR
       "Rec not well formed: "; print_ast ast>])
 
-(* Interprets the clauses of a let *)
+(* Interprets the clauses of a Let *)
 and let_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
   | [] -> []
   | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
@@ -574,6 +599,112 @@ and let_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
     anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR
       "Let not well formed: "; print_ast ast>])
 
+(* Interprets the clauses of a LetCutIn *)
+and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
+  | [] -> []
+  | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
+    (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t)::
+      (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+  | Node(_,"LETCUTCLAUSE",[Nvar(_,s);com;tce])::tl ->
+    let id = id_of_string s
+    and typ =
+      constr_of_Constr (unvarg
+      (val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
+    and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce in
+    (match tac with
+    | VArg (Constr csr) ->
+      (s,VArg (Constr (mkCast (csr,typ))))::
+      (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+    | VArg (Identifier id) ->
+      (try
+         (s,VArg (Constr (mkCast (constr_of_id id goalopt,typ))))::
+         (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+       with | Not_found ->
+         errorlabstrm "Tacinterp.letin_interp"
+         [< 'sTR "Term or tactic expected" >])
+    | _ ->
+      (try
+         let t = tactic_of_value tac in
+         let ndc =
+           (match goalopt with
+           | None -> Global.named_context ()
+           | Some g -> pf_hyps g) in
+         start_proof id Declare.NeverDischarge ndc typ;
+         by t;
+         let (_,({const_entry_body = pft; const_entry_type = _},_)) =
+           cook_proof () in
+         delete_proof id;
+         (s,VArg (Constr (mkCast (pft,typ))))::
+         (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
+       with | NotTactic ->
+         delete_proof id;
+         errorlabstrm "Tacinterp.letin_interp"
+         [< 'sTR "Term or tactic expected" >]))
+  | _ ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.letin_interp",
+    [<'sTR "LetIn not well formed: "; print_ast ast>])
+
+(* Interprets the clauses of a LetCut *)
+and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
+  | [] -> tclIDTAC
+  | Node(_,"LETCUTCLAUSE",[Nvar(_,s);com;tce])::tl ->
+    let id = id_of_string s
+    and typ =
+      constr_of_Constr (unvarg
+      (val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
+    and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce
+    and (ndc,ccl) =
+      match goalopt with
+      |	None -> 
+        errorlabstrm "Tacinterp.letcut_interp" [< 'sTR
+        "Do not use Let for toplevel definitions, use Lemma, ... instead" >]
+      |	Some g -> (pf_hyps g,pf_concl g) in
+    (match tac with
+    | VArg (Constr csr) ->
+      let cutt = interp_atomic "Cut" [Constr typ]
+      and exat = interp_atomic "Exact" [Constr csr] in
+      tclTHENS cutt [tclTHEN (introduction id)
+      (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat]
+
+(*      let lic = mkLetIn (Name id,csr,typ,ccl) in
+      let ntac = refine (mkCast (mkMeta (Environ.new_meta ()),lic)) in
+      tclTHEN ntac (tclTHEN (introduction id)
+      (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*)
+
+    | VArg (Identifier ir) ->
+      (try
+         let cutt = interp_atomic "Cut" [Constr typ]
+         and exat = interp_atomic "Exact" [Constr (constr_of_id ir goalopt)] in
+         tclTHENS cutt [tclTHEN (introduction id)
+         (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat]
+       with | Not_found ->
+         errorlabstrm "Tacinterp.letin_interp"
+         [< 'sTR "Term or tactic expected" >])
+    | _ ->
+      (try
+         let t = tactic_of_value tac in
+         start_proof id Declare.NeverDischarge ndc typ;
+         by t;
+         let (_,({const_entry_body = pft; const_entry_type = _},_)) =
+           cook_proof () in
+         delete_proof id;
+         let cutt = interp_atomic "Cut" [Constr typ]
+         and exat = interp_atomic "Exact" [Constr pft] in
+         tclTHENS cutt [tclTHEN (introduction id)
+         (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat]
+
+(*         let lic = mkLetIn (Name id,pft,typ,ccl) in
+         let ntac = refine (mkCast (mkMeta (Environ.new_meta ()),lic)) in
+         tclTHEN ntac (tclTHEN (introduction id)
+         (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*)
+       with | NotTactic ->
+         delete_proof id;
+         errorlabstrm "Tacinterp.letcut_interp"
+         [< 'sTR "Term or tactic expected" >]))
+  | _ ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.letcut_interp",[<'sTR
+      "LetCut not well formed: "; print_ast ast>])
+
 (* Interprets the Match Context expressions *)
 and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
   let goal =
@@ -725,16 +856,21 @@ and match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
 and tac_interp lfun lmatch debug ast g =
   let evc = project g
   and env = pf_env g in
-    match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with
+  try tactic_of_value (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) g
+  with | NotTactic ->
+    errorlabstrm "Tacinterp.tac_interp" [<'sTR
+    "Interpretation gives a non-tactic value">]
+
+(*    match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with
       | VTactic tac -> (tac g)
       | VFTactic (largs,f) -> (f largs g) 
       | VRTactic res -> res
       | _ ->
         errorlabstrm "Tacinterp.tac_interp" [<'sTR
-          "Interpretation gives a non-tactic value">]
+          "Interpretation gives a non-tactic value">]*)
 
 (* Interprets a primitive tactic *)
-and interp_atomic loc opn args = vernac_tactic(opn,args)
+and interp_atomic opn args = vernac_tactic(opn,args)
 
 (* Interprets sequences of tactics *)
 and interp_semi_list acc lfun lmatch debug = function
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index f7afda327b..852b0ff832 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -14,8 +14,6 @@ let v_transitivity  = hide_tactic "Transitivity"  dyn_transitivity
 let v_intro         = hide_tactic "Intro"         dyn_intro
 let v_intro_move    = hide_tactic "IntroMove"     dyn_intro_move
 let v_introsUntil   = hide_tactic "IntrosUntil"   dyn_intros_until
-(*i let v_tclIDTAC      = hide_tactic "Idtac"         dyn_tclIDTAC
-let v_tclFAIL       = hide_tactic "Fail"          dyn_tclFAIL i*)
 let v_assumption    = hide_tactic "Assumption"    dyn_assumption
 let v_exact         = hide_tactic "Exact"         dyn_exact_check
 let v_reduce        = hide_tactic "Reduce"        dyn_reduce
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 96dcfbb502..0348686072 100755
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2,10 +2,11 @@
 (* $Id$ *)
 
 (*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED *)
+
 Require Le.
 
 Parameter List_Dom:Set.
-Local A := List_Dom.
+Definition A := List_Dom.
 
 Inductive list : Set := nil : list | cons : A -> list -> list.
 
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 56077f36e5..b6824dac78 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -19,9 +19,15 @@ open Declare
 (* strength * strength -> bool *)
 
 let stre_gt = function
-  | (NeverDischarge,NeverDischarge) -> false
-  | (NeverDischarge,x) -> false
-  | (x,NeverDischarge) -> true
+(*  | (x,y) when (x = NeverDischarge || x = NotDeclare)
+            && (y = NeverDischarge || y = NotDeclare) -> false
+  | (x,_) when x = NeverDischarge || x = NotDeclare -> false
+  | (_,x) when x = NeverDischarge || x = NotDeclare -> true*)
+
+  | (NeverDischarge,_) -> false
+  | (NotDeclare,_) -> false
+  | (_,NeverDischarge) -> true
+  | (_,NotDeclare) -> true
   | (DischargeAt sp1,DischargeAt sp2) ->
       dirpath_prefix_of sp1 sp2 (* was sp_gt but don't understand why - HH *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 68d0455128..d1b9ba4fe1 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -17,6 +17,8 @@ open Ast
 open Library
 open Libobject
 open Astterm
+open Proof_type
+open Tacmach
 
 let mkCastC(c,t) = ope("CAST",[c;t])
 let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
@@ -77,6 +79,9 @@ let definition_body_red red_option ident (local,n) com comtypeopt =
         end
 	else
 	  declare_global_definition ident ce' n true
+    | NotDeclare ->
+      anomalylabstrm "Command.definition_body_red"
+        [<'sTR "Strength NotDeclare not for Definition, only for Let" >]
 
 let definition_body = definition_body_red None
 
@@ -113,6 +118,9 @@ let hypothesis_def_var is_refining ident n c =
         end
 	else
 	  declare_global_assumption ident c
+    | NotDeclare ->
+      anomalylabstrm "Command.hypothesis_def_var"
+        [<'sTR "Strength NotDeclare not for Variable, only for Let" >]
 
 (* 3| Mutual Inductive definitions *)
 
@@ -413,33 +421,52 @@ let start_proof_com sopt stre com =
   in
   Pfedit.start_proof id stre sign (interp_type Evd.empty env com)
 
-let save_named opacity =
-  let id,(const,strength) = Pfedit.cook_proof () in
+let apply_tac_not_declare id pft = function
+  | None -> error "Type of Let missing"
+  | Some typ ->
+    let cutt = vernac_tactic ("Cut",[Constr typ])
+    and exat = vernac_tactic ("Exact",[Constr pft]) in
+    Pfedit.delete_current_proof ();
+    Pfedit.by (tclTHENS cutt [introduction id;exat])
+
+let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
+  strength =
   begin match strength with
     | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
 	let c = constr_of_constr_entry const in
 	declare_variable id (SectionLocalDef c,strength,opacity)
-    | _ ->
-	declare_constant id (ConstantEntry const,strength,opacity)
+    | NeverDischarge | DischargeAt _ ->
+        declare_constant id (ConstantEntry const,strength,opacity)
+    | NotDeclare -> apply_tac_not_declare id pft tpo
   end;
-  Pfedit.delete_current_proof ();
-  if Options.is_verbose() then message ((string_of_id id) ^ " is defined")
+  if not (strength = NotDeclare) then
+  begin
+    Pfedit.delete_current_proof ();
+    if Options.is_verbose() then
+      message ((string_of_id id) ^ " is defined")
+  end
 
-let save_anonymous opacity save_ident strength =
-  let id,(const,_) = Pfedit.cook_proof () in
+let save_named opacity =
+  let id,(const,strength) = Pfedit.cook_proof () in
+  save opacity id const strength
+
+let save_anonymous_with_strength opacity save_ident id const strength =
   if atompart_of_id id <> "Unnamed_thm" then
     message("Overriding name "^(string_of_id id)^" and using "^save_ident);
-  declare_constant 
-    (id_of_string save_ident) (ConstantEntry const,strength,opacity);
-  Pfedit.delete_current_proof ();
-  if Options.is_verbose() then message (save_ident ^ " is defined")
+  save opacity (id_of_string save_ident) const strength
 
-let save_anonymous_thm opacity id =
-  save_anonymous opacity id NeverDischarge
+let save_anonymous opacity save_ident =
+  let id,(const,strength) = Pfedit.cook_proof () in
+  save_anonymous_with_strength opacity save_ident id const strength
+
+let save_anonymous_thm opacity save_ident =
+  let id,(const,_) = Pfedit.cook_proof () in
+  save_anonymous_with_strength opacity save_ident id const NeverDischarge
 
-let save_anonymous_remark opacity id =
-  let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
-  save_anonymous opacity id (make_strength path)
+let save_anonymous_remark opacity save_ident =
+  let id,(const,_) = Pfedit.cook_proof ()
+  and path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
+  save_anonymous_with_strength opacity save_ident id const (make_strength path)
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index abd42a87ea..44bf292667 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -51,6 +51,11 @@ fails if the proof is not completed *)
 
 val save_named : bool -> unit
 
+(* [save_anonymous b name] behaves as [save_named] but declares the theorem
+under the name [name] and respects the strength of the declaration *)
+
+val save_anonymous : bool -> string -> unit
+
 (* [save_anonymous_thm b name] behaves as [save_named] but declares the
 theorem under the name [name] and gives it the strength of a theorem *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7f3485e4eb..a37cfcf0b4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -3,6 +3,7 @@
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
+open Declarations
 open Pp
 open Util
 open Options
@@ -498,6 +499,24 @@ let _ =
        | _ -> bad_vernac_args "DefinedNamed")
 
 let _ =
+  add "DefinedAnonymous"
+    (function 
+       | [VARG_IDENTIFIER id] -> 
+	   (fun () -> 
+	      if not(is_silent()) then show_script();
+              save_anonymous false (string_of_id id))
+       | _ -> bad_vernac_args "DefinedAnonymous")
+
+let _ =
+  add "SaveAnonymous"
+    (function 
+       | [VARG_IDENTIFIER id] -> 
+	   (fun () -> 
+	      if not(is_silent()) then show_script();
+              save_anonymous true (string_of_id id))
+       | _ -> bad_vernac_args "SaveAnonymous")
+
+let _ =
   add "SaveAnonymousThm"
     (function 
        | [VARG_IDENTIFIER id] -> 
@@ -741,6 +760,7 @@ let _ =
              | "REMARK" -> make_strength_0 ()
              | "DEFINITION" -> NeverDischarge
              | "LET" -> make_strength_2 ()
+	     | "LETTOP" -> NotDeclare
              | "LOCAL" -> make_strength_0 ()
              | _       -> anomaly "Unexpected string"
            in 
@@ -769,6 +789,7 @@ let _ =
              | "REMARK" -> (make_strength_0(),true)
              | "DEFINITION" -> (NeverDischarge,false)
              | "LET" -> (make_strength_1(),false)
+	     | "LETTOP" -> (NeverDischarge,false)
              | "LOCAL" -> (make_strength_0(),false)
              | _       -> anomaly "Unexpected string" 
 	   in
@@ -780,10 +801,19 @@ let _ =
                      if not (is_silent()) then show_open_subgoals();
                      List.iter Vernacinterp.call calls;
                      if not (is_silent()) then show_script();
-                     save_named opacity)
+                     if not (kind = "LETTOP") then
+                       save_named opacity
+                     else
+                       let csr = interp_type Evd.empty (Global.env ()) com
+                       and (_,({const_entry_body = pft;
+                                const_entry_type = _},_)) = cook_proof () in
+                       let cutt = vernac_tactic ("Cut",[Constr csr])
+                       and exat = vernac_tactic ("Exact",[Constr pft]) in
+                       delete_proof s;
+                       by (tclTHENS cutt [introduction s;exat]))
 		  ()
               with e ->
-            	if is_unsafe "proof" then begin
+            	if (is_unsafe "proof") && not (kind = "LETTOP") then begin
                   mSGNL [< 'sTR "Warning: checking of theorem "; pr_id s;
                            'sPC; 'sTR "failed";
                            'sTR "... converting to Axiom" >];