Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.

May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).


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

6 files changed, 16 insertions, 9 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 38675da786..a815e5d2f8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -421,7 +421,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
   let v = array_map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
-  RRec(dl,RFix nvn,Array.of_list (List.rev lfi),
+  RRec(dl,RFix (Array.map (fun i -> i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index e6bdcbd9bb..8550258c45 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -28,6 +28,9 @@ open Reductionops
 val new_meta : unit -> metavariable
 val mk_new_meta : unit -> constr
 
+(* [new_untyped_evar] is a generator of unique evar keys *)
+val new_untyped_evar : unit -> existential_key
+
 (***********************************************************)
 (* Creating a fresh evar given their type and context *)
 val new_evar :
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7d0c926fac..df76f992d0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -232,8 +232,8 @@ let rec pretype tycon env isevars lvar = function
       evar_type_fixpoint loc env isevars names ftys vdefj;
       let fixj =
 	match fixkind with
-	  | RFix (vn,i as vni) ->
-	      let fix = (vni,(names,ftys,Array.map j_val vdefj)) in
+	  | RFix (vn,i) ->
+	      let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in
 	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkFix fix) ftys.(i)
 	  | RCoFix i -> 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index d07b83ebac..8a7946cd72 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -75,8 +75,8 @@ val constr_out : Dyn.t -> constr
  *)
 val pretype : 
   type_constraint -> env -> evar_defs ref -> 
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_judgment
+  var_map * (identifier * identifier option) list ->
+  rawconstr -> unsafe_judgment
 
 val pretype_type : 
   val_constraint -> env -> evar_defs ref ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d06395b09d..1c59004175 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -34,8 +34,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type fix_kind = RFix of (int array * int) | RCoFix of int
-
 type binder_kind = BProd | BLambda | BLetIn
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -73,6 +71,10 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
+and fix_recursion_order = RStructRec | RWfRec of rawconstr
+
+and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 11b43ddfcc..cbd215d85e 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -31,8 +31,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type fix_kind = RFix of (int array * int) | RCoFix of int
-
 type binder_kind = BProd | BLambda | BLetIn
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -70,6 +68,10 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
+and fix_recursion_order = RStructRec | RWfRec of rawconstr
+
+and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+
 val cases_predicate_names : 
   (rawconstr * (name * (loc * inductive * name list) option)) list -> name list