Si un fixpoint a plusieurs arguments, mais un seul de type inductif,

ce patch dispense d'ecrire le { struct .. }

En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, 
l'index de l'argument inductif devient un int option au lieu d'un int. 
Les deux cas possibles:
- Some n : les situations autorisées auparavant, a savoir {struct}
 explicite, ou bien un seul argument au total
- None : le cas nouveau, qui redonne un entier lors du passage de
 rawconstr à constr si l'on trouve effectivement un unique argument
 ayant un type inductif, et une erreur sinon.

Pour l'instant, on cherche l'inductif dans le type de manière
syntaxique, mais il est jouable de rajouter un poil de reduction
(au moins delta). 

Dans le détail, voici les coins que ce patch influence:

- parsing/g_xml.ml4: continue pour l'instant a attendre un index
  explicite via un element xml "recIndex"

- contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà
  un cas ctv_ID_OPT_NONE correspondant à l'absence de struct.  Par
  contre, dans le détail, le code pour un CFix utilise l'index de
  recurrence pour recouper au besoin le type du fixpoint en deux.
  Est-ce que je me gourre en supposant que si l'on a besoin de couper
  ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de
  l'impression d'un constr, et donc que l'index aura été correctement
  résolu ?

- contrib/subtac/subtac_command.ml:
- contrib/funind/indfun.ml:
  dans les deux cas, j'ai fait le service minimum, le struct reste
  obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas
  dur à adapter pour ceux qui comprennent ces parties.



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

5 files changed, 32 insertions, 29 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9c39878c7..ed9e1fa06 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -59,14 +59,13 @@ let rec mkCLambdaN loc bll c =
 
 let rec index_and_rec_order_of_annot loc bl ann =
   match names_of_local_assums bl,ann with
-    | [_], (None, r) -> 0, r
+    | [_], (None, r) -> Some 0, r
     | lids, (Some x, ro) ->
         let ids = List.map snd lids in
-        (try list_index (snd x) ids - 1, ro
+        (try Some (list_index (snd x) ids - 1), ro
         with Not_found ->
           user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
-    | _ -> user_err_loc(loc,"index_of_annot",
-      Pp.str "cannot guess decreasing argument of fix")
+    | _, (None, r) -> None, r
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 87f388a74..0a0df6fb2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -218,16 +218,15 @@ GEXTEND Gram
           let ni =
             match fst annot with
                 Some id ->
-                  (try list_index (Name id) names - 1
-                  with Not_found ->  Util.user_err_loc
-                      (loc,"Fixpoint",
-                       Pp.str "No argument named " ++ Nameops.pr_id id))
+                  (try Some (list_index (Name id) names - 1)
+                   with Not_found ->  Util.user_err_loc
+                     (loc,"Fixpoint",
+                      Pp.str "No argument named " ++ Nameops.pr_id id))
               | None -> 
-                  if List.length names > 1 then
-                    Util.user_err_loc
-                      (loc,"Fixpoint",
-                       Pp.str "the recursive argument needs to be specified");
-                  0 in
+		  (* If there is only one argument, it is the recursive one, 
+		     otherwise, we search the recursive index later *)
+		  if List.length names = 1 then Some 0 else None	  
+	  in 
 	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
   ;
   corec_definition:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 1df3d1f25..8b3661dbe 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -205,11 +205,11 @@ and interp_xml_recursionOrder x =
 and interp_xml_FixFunction x =
   match interp_xml_tag "FixFunction" x with
   | (loc,al,[x1;x2;x3]) ->
-      ((nmtoken (get_xml_attr "recIndex" al),
+      ((Some (nmtoken (get_xml_attr "recIndex" al)),
 	interp_xml_recursionOrder x1),
        (get_xml_ident al, interp_xml_type x2, interp_xml_body x3))
   | (loc,al,[x1;x2]) -> (* For backwards compatibility *)
-      ((nmtoken (get_xml_attr "recIndex" al), RStructRec),
+      ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
        (get_xml_ident al, interp_xml_type x1, interp_xml_body x2))
   | (loc,_,_) -> 
         user_err_loc (loc,"",str "wrong number of arguments (expect one)")
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a95fa4bad..e4cc3cd91 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -379,11 +379,11 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
     let ids = names_of_local_assums bl in
       match ro with
 	  CStructRec ->
-	    if List.length ids > 1 then 
-	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
+	    if List.length ids > 1 && n <> None then 
+	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
 	    else mt() 
 	| CWfRec c ->
-	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}"
+	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c08b07617..f43f93bd9 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -555,18 +555,23 @@ let rec pr_vernac = function
               else ([],def,type_) in
             let bl = bl @ bl' in
             let ids = List.flatten (List.map name_of_binder bl) in
-            let name =
-              try snd (List.nth ids n)
-              with Failure _ ->
-                warn (str "non-printable fixpoint \""++pr_id id++str"\"");
-                Anonymous in
             let annot =
-	      match (ro : Topconstr.recursion_order_expr) with
-		  CStructRec -> 
-		    if List.length ids > 1 then 
-                      spc() ++ str "{struct " ++ pr_name name ++ str"}"
-		    else mt()
-		| CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}"
+	      match n with 
+		| None -> mt () 
+		| Some n -> 
+		    let name =
+		      try snd (List.nth ids n)
+		      with Failure _ ->
+			warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+			Anonymous in
+		    match (ro : Topconstr.recursion_order_expr) with
+			CStructRec -> 
+			  if List.length ids > 1 then 
+			    spc() ++ str "{struct " ++ pr_name name ++ str"}"
+			  else mt()
+		      | CWfRec c -> 
+			  spc() ++ str "{wf " ++ pr_name name ++ spc() ++ 
+			    pr_lconstr_expr c ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_