Added support for definition of fixpoints using tactics.

Fixed some bugs in -beautify and robustness of {struct} clause.

Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.



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

3 files changed, 27 insertions, 16 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 85f84b850f..e819e70099 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1048,11 +1048,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
 	     let intern_ro_arg f =
-	       let idx =
-		 match n with
-		     Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
-		   | None -> 0
-	       in
+               let idx = Option.default 0 (index_of_annot bl n) in
 	       let before, after = list_chop idx bl in
 	       let ((ids',_,_,_) as env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a6b4b1b0ab..ecb61e15b0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -639,8 +639,8 @@ type cases_pattern_expr =
 
 type constr_expr =
   | CRef of reference
-  | CFix of loc * identifier located * fixpoint_expr list
-  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CFix of loc * identifier located * fix_expr list
+  | CCoFix of loc * identifier located * cofix_expr list
   | CArrow of loc * constr_expr * constr_expr
   | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
@@ -667,7 +667,7 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr =
+and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
@@ -678,7 +678,7 @@ and typeclass_constraint = name located * binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
-and cofixpoint_expr =
+and cofix_expr =
     identifier located * local_binder list * constr_expr * constr_expr
 
 and recursion_order_expr =
@@ -918,6 +918,19 @@ let coerce_to_name = function
         (constr_loc a,"coerce_to_name",
          str "This expression should be a name.")
 
+(* Interpret the index of a recursion order annotation *)
+
+let index_of_annot bl na =
+  let names = List.map snd (names_of_local_assums bl) in
+  match na with
+  | None ->
+      if names = [] then error "A fixpoint needs at least one parameter." 
+      else None
+  | Some (loc, id) ->
+      try Some (list_index0 (Name id) names)
+      with Not_found ->
+        user_err_loc(loc,"",
+        str "No parameter named " ++ Nameops.pr_id id ++ str".")
 
 (* Used in correctness and interface *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1c0b207eab..b7e389d6b3 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -125,8 +125,8 @@ type cases_pattern_expr =
 
 type constr_expr =
   | CRef of reference
-  | CFix of loc * identifier located * fixpoint_expr list
-  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CFix of loc * identifier located * fix_expr list
+  | CCoFix of loc * identifier located * cofix_expr list
   | CArrow of loc * constr_expr * constr_expr
   | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
@@ -153,10 +153,10 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr =
+and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
-and cofixpoint_expr =
+and cofix_expr =
     identifier located * local_binder list * constr_expr * constr_expr
 
 and recursion_order_expr =
@@ -205,6 +205,8 @@ val coerce_reference_to_id : reference -> identifier
 val coerce_to_id : constr_expr -> identifier located
 val coerce_to_name : constr_expr -> name located
 
+val index_of_annot : local_binder list -> identifier located option -> int option
+
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
@@ -220,12 +222,12 @@ val local_binders_length : local_binder list -> int
 (* Excludes let binders *)
 val local_assums_length : local_binder list -> int
 
-(* Does not take let binders into account *)
-val names_of_local_assums : local_binder list -> name located list
-
 (* With let binders *)
 val names_of_local_binders : local_binder list -> name located list
 
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
 (* Used in typeclasses *)
 
 val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->