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

3 files changed, 3 insertions, 3 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2057eb5b27..0be6b9dc6f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -793,7 +793,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
 		     RStructRec,
 		     List.fold_left intern_local_binder (env,[]) bl
 		 | CWfRec c -> 
-		     let before, after = list_chop (succ n) bl in
+		     let before, after = list_chop (succ (out_some n)) bl in
 		     let ((ids',_,_),rafter) =
 		       List.fold_left intern_local_binder (env,[]) after in
 		     let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 4d4e3f88a0..d82c04e077 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -532,7 +532,7 @@ type constr_expr =
 
 
 and fixpoint_expr =
-    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 073f9ba0b3..4e2017f44d 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -114,7 +114,7 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr