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

9 files changed, 71 insertions, 25 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 5224190301..bf5aed32e8 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 0016bfdaf2..46121ff182 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 34d9f62067..30ecc8ff76 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 cea3fbf514..fd93a115ae 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 16363ac673..f75dd5c396 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 4a17195281..42de8cb89a 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} 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 4e54044473..2e2804cf2b 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -209,6 +209,8 @@ let all_entries () =
 }
 
 (*s Shortcuts for regular expressions. *)
+let digit = ['0'-'9']
+let num = digit+
 
 let space = 
   [' ' '\010' '\013' '\009' '\012']
@@ -225,16 +227,18 @@ let end_hide = "(*" space* "end" space+ "hide" space* "*)"
 (*s Indexing entry point. *)
   
 rule traverse = parse
-  | "Definition" space
+  | ("Program" space+)? "Definition" space
       { current_type := Definition; index_ident lexbuf; traverse lexbuf }
   | "Tactic" space+ "Definition" space
       { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf }
   | ("Axiom" | "Parameter") space 
       { current_type := Axiom; index_ident lexbuf; traverse lexbuf }
-  | "Fixpoint" space
+  | ("Program" space+)? "Fixpoint" space
       { current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
 	traverse lexbuf }
-  | ("Lemma" | "Theorem") space
+  | ("Program" space+)? ("Lemma" | "Theorem") space
+      { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
+  | "Obligation" space num ("of" ident)?
       { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
   | "Inductive" space
       { current_type := Inductive; 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 8ac25ad269..737cd4d755 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -43,12 +43,15 @@ let is_keyword =
       "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
       "Unset"; "Variable"; "Variables"; 
       "Notation"; 
+      (* Program *)
+      "Program Definition"; "Program Fixpoint"; "Program Lemma";
+      "Obligation"; "Obligations"; "Solve";
       (*i (* correctness *)
       "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if";
       "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant";
       "while"; i*)
-      (*i (* coq terms *)
-      "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*)
+      (*i (* coq terms *) *)
+	"match"; "with"; "end"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
        ]
 
 (*s Current Coq module *)
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 869df4eef6..80cdb321be 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -257,8 +257,15 @@ let extraction =
   | "Recursive" space+ "Extraction" 
   | "Extract"
 
+
 let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
 
+let prog_kw =
+  "Program" space+ gallina_kw
+  | "Obligation"
+  | "Obligations"
+  | "Solve"
+
 let gallina_kw_to_hide =
   "Implicit"
   | "Ltac"
@@ -344,6 +351,15 @@ rule coq_bol = parse
 	    ident s (lexeme_start lexbuf + nbsp); 
 	    let eol= body lexbuf in
 	      if eol then coq_bol lexbuf else coq lexbuf }
+  | space* prog_kw
+      { let s = lexeme lexbuf in 
+	let nbsp = count_spaces s in
+	  indentation nbsp;
+	  let s = String.sub s nbsp (String.length s - nbsp)  in
+	    ident s (lexeme_start lexbuf + nbsp); 
+	    let eol= body lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf }
+
   | space* "(**" space+ "printing" space+ (identifier | token) space+
       { let tok = lexeme lexbuf in
 	let s = printing_token lexbuf in
@@ -414,6 +430,11 @@ and coq = parse
 	  ident s (lexeme_start lexbuf); 
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
+  | prog_kw
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); 
+	let eol = body lexbuf in
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | space+ { char ' '; coq lexbuf }
   | eof 
       { () }