numarg -> pure_numarg a poursuivre

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

4 files changed, 62 insertions, 50 deletions

diff --git a/PROBLEMES b/PROBLEMES
index aed1579124..ff4e7e5825 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -9,14 +9,30 @@ l'application de la tactique, ils ne peuvent pas contenir des variables
 qui seront introduites dans la tactique ....
 MUTUAL-EXCLUSION/binary/version1/Soundness.v
 
-l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les binding je pense) 
-d'ou des erreurs de syntaxe ...
-pure_numarg est plus sur
+l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les
+binding je pense) d'ou des erreurs de syntaxe ...  pure_numarg est
+plus sūr
 
 Associativite Repeat Orelse changee
 	Repeat A Orelse B se lit (Repeat A) Orelse B 
 ce n'est pas malin car Repeat A n'echoue jamais
 
+Probleme de Reset Initial.
+Load Field.
+Reset Initial.
+Coq <  Load Field.
+Error while reading ./Field.v :
+File "./Field.v", line 6, characters 0-83
+Error: list already exists
+(* l'erreur ne se produit pas sur un fichier plus court ..)
+voir dans library states.ml 
+la fonction freeze=set_state qui modifie l'etat initial ....
+
+les parentheses ne sont pas autorises autour de 
+motifs constants :
+> Check [n:nat]Cases n of (O) => true | _ => false end.
+Syntax error: 'as' or ',' or [ne_pattern_list] expected after [Constr.pattern] (in [compound_pattern])
+
 CONTRIBS
 ---------
 BellLabs/lazyPCF : OK
@@ -42,10 +58,16 @@ Lyon/IEEE754 : OK
 Lyon/COINDUCTIVES : OK
 
 Rocq/GRAPHS
-File "./lsort.v", line 82, characters 4-17
-Error: Impossible to unify ad with
- (a:ad)(?334 a)->(?334 (ad_double_plus_un a))
-Induction a.
+/home/cpaulin/TYPES/V7/bin/coqc  -q  -I . lsort
+Warning: compute_metamap: MV(1506) sans type !
+Utilise NewInduction
+
+/home/cpaulin/TYPES/V7/bin/coqc  -q  -I . cgraph
+Warning: Found several default clauses, kept the first one
+
+File "./cgraph.v", line 1866, characters 2-7
+Error: frontier was handed back a ill-formed proof.
+(Apres un EApply)
 
 Rocq/MUTUAL-EXCLUSION/
 	Incompatibilite interpretation des arguments de Tactic Definition
@@ -76,18 +98,14 @@ File "./Functions.v", line 95, characters 0-15
 Error: Bad inductive definition.
 A la fermeture de section
 
-Rocq/RATIONAL
-	Rewrite/LeibnizRewrite
-/home/cpaulin/coq/V7/bin/coqc  -q -byte -I . -I ../MLstuff HS
-[Loading ML file struct.cmo ...done]
-[Loading ML file sort_tac.cmo ...failed]
-File "./HS.v", line 6, characters 0-30
-Error: Cannot link ml-object sort_tac.cmo to Coq code.
-
 Rocq/SUBST
 File "./TS.v", line 69, characters 0-6
 Error: Attempt to save an incomplete proof
 
+Rocq/DEMOS/Demo_AutoRewrite
+Anomaly: Invalid argument "output_value: functional value".
+
+
 Montevideo/CtlTctl OK
 Montevideo/RailroadCrossing
 File "./railroad_crossing.v", line 613, characters 2-20
diff --git a/TODO b/TODO
index 43ff76050f..36a7283d35 100644
--- a/TODO
+++ b/TODO
@@ -23,6 +23,7 @@ Vernac:
 Grammaires:
 
 - pb avec les extensions constr (cf Zsyntax et Cases x of `0` => ...)
+- revoir numarg/pure_numarg dans g_tactic.ml4 (regles a factoriser)
 
 Doc:
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 134287b3ed..f502f860ba 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -101,7 +101,7 @@ GEXTEND Gram
   ;
   simple_binding:
     [ [ id = identarg; ":="; c = constrarg -> <:ast< (BINDING $id $c) >>
-      | n = numarg; ":="; c = constrarg -> <:ast< (BINDING $n $c) >> ] ]
+      | n = pure_numarg; ":="; c = constrarg -> <:ast< (BINDING $n $c) >> ] ]
   ;
   simple_binding_list:
     [ [ b = simple_binding; l = simple_binding_list -> b :: l | -> [] ] ]
@@ -169,7 +169,7 @@ GEXTEND Gram
       | -> <:ast< (CLAUSE) >> ] ]
   ;
   autoarg_depth:
-  [ [ n = numarg -> <:ast< $n>>
+  [ [ n = pure_numarg -> <:ast< $n>>
      | -> Coqast.Str(loc,"NoAutoArg") ] ]
   ;
   autoarg_adding:
@@ -186,7 +186,7 @@ GEXTEND Gram
       | -> Coqast.Str(loc,"NoAutoArg")  ] ]
   ;
   fixdecl:
-    [ [ id = identarg; n = numarg; ":"; c = constrarg; fd = fixdecl ->
+    [ [ id = identarg; n = pure_numarg; ":"; c = constrarg; fd = fixdecl ->
           <:ast< (FIXEXP $id $n $c) >> :: fd
       | -> [] ] ]
   ;
@@ -281,11 +281,11 @@ GEXTEND Gram
       |	IDENT "Try"; ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
         <:ast< (TRY (ORELSE $ta0 $ta1)) >>
       |	IDENT "Try"; ta = tactic_atom -> <:ast< (TRY $ta) >>
-      | IDENT "Do"; n = numarg; ta = tactic_atom -> <:ast< (DO $n $ta) >>
+      | IDENT "Do"; n = pure_numarg; ta = tactic_atom -> <:ast< (DO $n $ta) >>
       | IDENT "Repeat"; ta = tactic_atom -> <:ast< (REPEAT $ta) >>
       |	IDENT "Idtac" -> <:ast< (IDTAC) >>
       |	IDENT "Fail" -> <:ast<(FAIL)>>
-      |	IDENT "Fail"; n = numarg -> <:ast<(FAIL $n)>>
+      |	IDENT "Fail"; n = pure_numarg -> <:ast<(FAIL $n)>>
       |	ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
           <:ast< (ORELSE $ta0 $ta1) >>
       |	st = simple_tactic -> st
@@ -307,35 +307,35 @@ GEXTEND Gram
            |_ -> c) ] ]
   ;
   simple_tactic:
-    [ [ IDENT "Fix"; n = numarg -> <:ast< (Fix $n) >>
-      | IDENT "Fix"; id = identarg; n = numarg -> <:ast< (Fix $id $n) >>
-      | IDENT "Fix"; id = identarg; n = numarg; "with"; fd = fixdecl ->
+    [ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >>
+      | IDENT "Fix"; id = identarg; n = pure_numarg -> <:ast< (Fix $id $n) >>
+      | IDENT "Fix"; id = identarg; n = pure_numarg; "with"; fd = fixdecl ->
           <:ast< (Fix $id $n ($LIST $fd)) >>
       | IDENT "Cofix" -> <:ast< (Cofix) >>
       | IDENT "Cofix"; id = identarg -> <:ast< (Cofix $id) >>
       | IDENT "Cofix"; id = identarg; "with"; fd = cofixdecl ->
           <:ast< (Cofix $id ($LIST $fd)) >>
       | IDENT "Induction"; s = identarg -> <:ast< (Induction $s) >>
-      | IDENT "Induction"; n = numarg -> <:ast< (Induction $n) >>
+      | IDENT "Induction"; n = pure_numarg -> <:ast< (Induction $n) >>
       | IDENT "NewInduction"; c = constrarg -> <:ast< (NewInduction $c) >>
-      | IDENT "NewInduction"; n = numarg -> <:ast< (NewInduction $n) >>
+      | IDENT "NewInduction"; n = pure_numarg -> <:ast< (NewInduction $n) >>
       | IDENT "Double"; IDENT "Induction"; i = numarg; j = numarg ->
           <:ast< (DoubleInd $i $j) >>
       | IDENT "Trivial" -> <:ast<(Trivial)>>
       | IDENT "Trivial"; "with"; lid = ne_identarg_list -> 
 	  <:ast<(Trivial ($LIST $lid))>>
       | IDENT "Trivial"; "with"; "*" ->  <:ast<(Trivial "*")>>
-      | IDENT "Auto"; n = numarg -> <:ast< (Auto $n) >>
+      | IDENT "Auto"; n = pure_numarg -> <:ast< (Auto $n) >>
       | IDENT "Auto" -> <:ast< (Auto) >>
-      | IDENT "Auto"; n = numarg; "with";
+      | IDENT "Auto"; n = pure_numarg; "with";
 	  lid = ne_identarg_list -> <:ast< (Auto $n ($LIST $lid)) >>
       | IDENT "Auto"; "with";
 	  lid = ne_identarg_list -> <:ast< (Auto ($LIST $lid)) >>
-      | IDENT "Auto"; n = numarg; "with"; "*" ->
+      | IDENT "Auto"; n = pure_numarg; "with"; "*" ->
 	  <:ast< (Auto $n "*") >>
       | IDENT "Auto"; "with"; "*" -> <:ast< (Auto "*") >>
      
-      | IDENT "AutoTDB"; n = numarg -> <:ast< (AutoTDB $n) >>
+      | IDENT "AutoTDB"; n = pure_numarg -> <:ast< (AutoTDB $n) >>
       | IDENT "AutoTDB" -> <:ast< (AutoTDB) >>
       | IDENT "DHyp";  id=identarg  -> <:ast< (DHyp  $id)>>
       | IDENT "CDHyp"; id=identarg -> <:ast<  (CDHyp $id)>>
@@ -346,9 +346,9 @@ GEXTEND Gram
                        a2 = autoarg_destructing; 
                        a3 = autoarg_usingTDB -> 
                    <:ast< (SuperAuto $a0 $a1 $a2 $a3) >>
-      | IDENT "Auto"; n = numarg; IDENT "Decomp" -> <:ast< (DAuto $n) >>
+      | IDENT "Auto"; n = pure_numarg; IDENT "Decomp" -> <:ast< (DAuto $n) >>
       | IDENT "Auto"; IDENT "Decomp" -> <:ast< (DAuto) >>
-      | IDENT "Auto"; n = numarg; IDENT "Decomp"; p = numarg ->
+      | IDENT "Auto"; n = pure_numarg; IDENT "Decomp"; p = pure_numarg ->
           <:ast< (DAuto $n $p) >>
       ] ];
     END
@@ -390,7 +390,7 @@ GEXTEND Gram
       | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg ->
           <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
       | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >>
-      | IDENT "Specialize"; n = numarg; lcb = constrarg_binding_list ->
+      | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
       | IDENT "Specialize"; lcb = constrarg_binding_list ->
           <:ast< (Specialize ($LIST $lcb)) >>
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 2c9185349d..3bbe2d19c1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -48,7 +48,7 @@ let usage () =
 
 coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
   command dependencies file] ... [-I dir] ... [VARIABLE = value] ...
-  [-full] [-no-opt] [-f file] [-o file] [-h] [--help]
+  [-opt|-byte] [-f file] [-o file] [-h] [--help]
 
 [file.v]: Coq file to be compiled
 [file.ml]: ML file to be compiled
@@ -57,8 +57,8 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
   \"command\" and dependencies \"dependencies\"
 [-I dir]: look for dependencies in \"dir\"
 [VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
-[-full]: \"opt\" should use \"coqc -full\" instead of \"coqc -opt\"
-[-no-opt]: target \"opt\" should be equivalent to \"byte\"
+[-byte]: compile with byte-code version of coq
+[-opt]: compile with native-code version of coq
 [-f file]: take the contents of file as arguments
 [-o file]: output should go in file file 
 [-h]: print this usage summary
@@ -77,7 +77,6 @@ let standard sds =
     print "\trm .depend\n";
     print "\t$(COQDEP) -i $(LIBS) *.v *.ml *.mli >.depend\n";
     print "\t$(COQDEP) $(LIBS) -suffix .html *.v >>.depend\n";
-    if !some_mlfile then print "\t$(P4DEP) *.ml >>.depend\n"
   end;
   List.iter
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n")
@@ -113,8 +112,6 @@ let implicit () =
     print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n" ;
     print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n" ;
     print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n" ;
-    print ".ml4.cmo:\n\t$(CAMLC) -pp $(P4) $(ZDEBUG) $(ZFLAGS) -impl $<\n\n";
-    print ".ml4.cmx:\n\t$(CAMLOPTC) -pp $(P4) $(ZDEBUG) $(ZFLAGS)\n\n"
   and v_rule () =
     print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n" ;
     print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n" ;
@@ -153,12 +150,11 @@ let variables l =
   section "Variables definitions.";
   print "CAMLP4LIB=`camlp4 -where`\n";
   print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n";
-  print "COQSRC=-I $(COQTOP)/src/tactics -I $(COQTOP)/src/proofs \\
-  -I $(COQTOP)/src/syntax -I $(COQTOP)/src/env -I $(COQTOP)/src/lib/util \\
-  -I $(COQTOP)/src/constr -I $(COQTOP)/tactics -I $(COQTOP)/src/meta \\
-  -I $(COQTOP)/src/parsing -I $(COQTOP)/src/typing -I $(CAMLP4LIB)\n";
+  print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
+  -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \\
+  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\
+  -I $(COQTOP)/toplevel -I $(CAMLP4LIB)\n";
   print "ZFLAGS=$(LIBS) $(COQSRC)\n";
-  print "FULLOPT=$(OPT:-opt=-full)\n";
   if !opt="-opt" then
     print "COQFLAGS=-q $(OPT) $(LIBS)\n"
   else begin
@@ -176,9 +172,6 @@ let variables l =
   print "CAMLLINK=ocamlc\n";
   print "CAMLOPTLINK=ocamlopt\n";
   print "COQDEP=$(COQBIN)coqdep -c\n";
-  print "P4=$(COQBIN)call_camlp4 -I $(COQTOP)/src/parsing \\
-  -I $(COQTOP)/theories/INIT -I $(COQTOP)/tactics\n";
-  print "P4DEP=$(COQBIN)camlp4dep\n";
   var_aux l;
   print "\n"
 
@@ -299,10 +292,10 @@ let rec process_cmd_line = function
       some_file := !some_file or !some_mlfile or !some_vfile ; []
   | ("-h"|"--help") :: _ -> 
       usage ()
-  | "-no-opt" :: r -> 
-      opt := "" ; process_cmd_line r
-  | "-full"::r -> 
-      opt := "-full" ; process_cmd_line r
+  | ("-no-opt"|"-byte") :: r -> 
+      opt := "-byte" ; process_cmd_line r
+  | ("-full"|"-opt")::r -> 
+      opt := "-opt" ; process_cmd_line r
   | "-custom" :: com :: dependencies :: file :: r ->
       some_file := true;
       Special (file,dependencies,com) :: (process_cmd_line r)