Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.

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

6 files changed, 38 insertions, 20 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 522419030..bf5aed32e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1929,6 +1929,7 @@ let rec xlate_vernac =
 	     xlate_sort sort) in
         CT_ind_scheme
 	  (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
+   | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
    | VernacSyntacticDefinition (id, c, false, _) ->
        CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
    | VernacSyntacticDefinition (id, c, true, _) ->
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 0016bfdaf..46121ff18 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -2,13 +2,13 @@ Require Import Wf.
 Require Import Coq.subtac.Utils.
 
 Section Well_founded.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : A -> A -> Prop.
   Hypothesis Rwf : well_founded R.
   
   Section Acc.
     
-    Variable P : A -> Set.
+    Variable P : A -> Type.
     
     Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
     
@@ -20,7 +20,7 @@ Section Well_founded.
   End Acc.
   
   Section FixPoint.
-    Variable P : A -> Set.
+    Variable P : A -> Type.
     
     Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
     
@@ -75,13 +75,13 @@ Require Import Wf_nat.
 Require Import Lt.
 
 Section Well_founded_measure.
-Variable A : Set.
+Variable A : Type.
 Variable f : A -> nat.
 Definition R := fun x y => f x < f y.
 
 Section FixPoint.
 
-Variable P : A -> Set.
+Variable P : A -> Type.
 
 Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
  
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 34d9f6206..30ecc8ff7 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -66,5 +66,9 @@ Ltac destruct_call f :=
     end.
 
 Extraction Inline proj1_sig.
+Extract Inductive unit => "unit" [ "()" ].
+Extract Inductive bool => "bool" [ "true" "false" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extract Inductive prod => "" [ "" ].
 
 Require Export ProofIrrelevance.
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index cea3fbf51..fd93a115a 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1187,6 +1187,7 @@ let group_equations pb ind current cstrs mat =
 let rec generalize_problem pb = function
   | [] -> pb
   | i::l ->
+      trace (str"Generalizing problem");
       let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
       let pb' = generalize_problem pb l in
       let tomatch = lift_tomatch_stack 1 pb'.tomatch in
@@ -1272,10 +1273,11 @@ let build_branch current deps pb eqns const_info =
 
   let cur_alias = lift (List.length sign) current in
   let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
-
-  sign,
+  let env' = push_rels sign pb.env in
+  let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
+    sign,
   { pb with
-      env = push_rels sign pb.env;
+      env = env';
       tomatch = List.rev_append currents tomatch;
       pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
       history = history;
@@ -1640,14 +1642,13 @@ let constr_of_pat env isevars ty pat =
 	let app = applistc cstr (List.map (lift (List.length args)) params) in
 	let app = applistc app args in
 (* 	  trace (str "New pattern: " ++ Printer.pr_cases_pattern pat'); *)
+	let alname = if alias <> Anonymous then alias else Name (id_of_string "anon") in
+	let al = alname, Some (mkRel 1), lift 1 ty in
 	  if alias <> Anonymous then
 	    pat', (alias, Some app, ty) :: sign, lift 1 app, n + 1
 	  else pat', sign, app, n
   in 
   let pat', sign, y, z = typ env ty pat in 
-(*   let prod = it_mkProd_or_LetIn y sign in *)
-(*     trace (str "Pattern: " ++ Printer.pr_cases_pattern pat ++ str " becomes constr : " ++ *)
-(* 	     my_print_constr env prod); *)
     pat', (sign, y)
 
 let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |])
@@ -1766,9 +1767,12 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
  * A type constraint but no annotation case: it is assumed non dependent.
  *)
 
-let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon = 
+let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs arsign tycon = 
   (* We extract the signature of the arity *)
-  let arsign = extract_arity_signature env tomatchs sign in
+  List.iter
+      (fun arsign -> 
+	 trace (str "arity signature: " ++ my_print_rel_context env arsign))
+    arsign;
 (*   let env = List.fold_right push_rels arsign env in *)
   let allnames = List.rev (List.map (List.map pi1) arsign) in
   let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
@@ -1823,8 +1827,12 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	None ->	  
 	  let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in
 	  let matx = List.rev matx in
-	  let env = push_rels lets env in
 	  let len = List.length lets in
+	  let sign = 
+	    let arsign = extract_arity_signature env tomatchs (List.map snd tomatchl) in
+	      List.map (lift_rel_context len) arsign
+	  in
+	  let env = push_rels lets env in	      
 	  let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
 	  let tycon = lift_tycon len tycon in
 	  let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
@@ -1832,9 +1840,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	    
 	  (* We build the elimination predicate if any and check its consistency *)
 	  (* with the type of arguments to match *)
-	  let tmsign = List.map snd tomatchl in
-	  let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs tmsign tycon in
-	    
+	  let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon in
 	  (* We push the initial terms to match and push their alias to rhs' envs *)
 	  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
 	  let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
@@ -1883,5 +1889,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	    (* We check for unused patterns *)
 	    List.iter (check_unused_pattern env) matx;
 	    inh_conv_coerce_to_tycon loc env isevars j tycon	  
+
 end
   
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 16363ac67..f75dd5c39 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -244,15 +244,17 @@ module Coercion = struct
 			   coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x))
 		       else co
 		     in
-		       if Array.length l = Array.length l' then
+		       if Array.length l = Array.length l' then (
+			 trace (str"Inserting coercion at application");
 			 Some (coerce lam_type 0 (fun x -> x))
-		       else subco ()
+		       ) else subco ()
 		 | _ -> subco ())
 	  | _, _ ->  subco ()
 
     and subset_coerce env isevars x y =
       match disc_subset x with
 	  Some (u, p) -> 
+	    (* trace (str "Inserting projection ");	     *)
 	    let c = coerce_unify env u y in
 	    let f x = 
 	      app_opt c (mkApp ((Lazy.force sig_).proj1, 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 4a1719528..42de8cb89 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -111,8 +111,12 @@ let subst_body prg =
     subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body
 
 let declare_definition prg =
+  let body = subst_body prg in
+    (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
+		  my_print_constr (Global.env()) body);
+     with _ -> ());
   let ce = 
-    { const_entry_body = subst_body prg;
+    { const_entry_body = body;
       const_entry_type = Some prg.prg_type;
       const_entry_opaque = false;
       const_entry_boxed = false}