Add a parameter to QuestionMark evar kind to say it can be turned into an obligations (even an opaque one).

Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.


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

12 files changed, 85 insertions, 66 deletions

diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
index 07a19ab376..4610f3467a 100644
--- a/contrib/subtac/FunctionalExtensionality.v
+++ b/contrib/subtac/FunctionalExtensionality.v
@@ -1,3 +1,11 @@
+Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+Qed.
+
 Axiom fun_extensionality : forall A B (f g : A -> B), 
   (forall x, f x = g x) -> f = g.
 
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index e678cf5d93..e1c48769c4 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -24,14 +24,19 @@ Ltac induction_with_subterms c c' H :=
 
 Ltac destruct_one_pair :=
  match goal with
- | [H : (ex _) |- _] => destruct H
- | [H : (ex2 _) |- _] => destruct H
- | [H : (sig _) |- _] => destruct H
- | [H : (_ /\ _) |- _] => destruct H
- | [H : prod _ _ |- _] => destruct H
-end.
+   | [H : (ex2 _) |- _] => destruct H
+   | [H : (_ /\ _) |- _] => destruct H
+   | [H : prod _ _ |- _] => destruct H
+ end.
 
-Ltac destruct_exists := repeat (destruct_one_pair) .
+Ltac destruct_one_ex :=
+  let tac H := let ph := fresh "H" in destruct H as [H ph] in
+    match goal with
+      | [H : (ex _) |- _] => tac H
+      | [H : (sig ?P) |- _ ] => tac H
+    end.
+
+Ltac destruct_exists := repeat (destruct_one_pair || destruct_one_ex).
 
 Ltac on_call f tac :=
   match goal with
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 6250794526..bf4876a03c 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -2,58 +2,37 @@ Require Export Coq.subtac.SubtacTactics.
 
 Set Implicit Arguments.
 
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
-
 Notation " {{ x }} " := (tt : { y : unit | x }).
 
-Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+Notation "{ ( x , y )  :  A  |  P }" := 
+  (sig (fun t:A => let (x,y) := t in P))
+  (x ident, y ident) : type_scope.
 
 Notation " ! " := (False_rect _ _).
 
-Require Import Coq.Bool.Sumbool.	
-Notation "'dec'" := (sumbool_of_bool) (at level 0). 
-
-Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
-intros.
-induction t.
-exact x.
-Defined.
+Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
+Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
 
-Lemma ex_pi2  : forall (A : Prop) (P : A -> Prop) (t : ex P),
- P (ex_pi1 t).
-intros A P.
-dependent inversion t.
-simpl.
-exact p.
-Defined.
+(** Coerces objects before comparing them *)
+Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
 
+(** Quantifying over subsets *)
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
 
-Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
 Notation "'forall' { x : A | P } , Q" :=
   (forall x:{x:A|P}, Q)
   (at level 200, x ident, right associativity).
 
-Lemma subset_simpl : forall (A : Set) (P : A -> Prop) 
-	(t : sig P), P (` t).
-Proof.
-intros.
-induction t.
- simpl ; auto.
-Qed.
-
-Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
-  f = g -> forall x, f x = g x.
-Proof.
-  intros.
-  rewrite H.
-  auto.
-Qed.
+Require Import Coq.Bool.Sumbool.	
+Notation "'dec'" := (sumbool_of_bool) (at level 0). 
 
+(** Default simplification tactic. *)
 Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; 
-  try (solve [ red ; intros ; discriminate ]) ; auto with arith.  
+  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
 
+(** Extraction directives *)
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index e0711cade9..1989e7dcf0 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -65,7 +65,8 @@ let subst_evar_constr evs n t =
 	     and we must not apply to defined ones (i.e. LetIn's)
 	  *)
 	let args = 
-	  let (l, r) = list_split_at chop (List.rev (Array.to_list args)) in
+	  let n = match chop with None -> 0 | Some c -> c in 
+	  let (l, r) = list_split_at n (List.rev (Array.to_list args)) in
 	    List.rev r
 	in
 	let args =
@@ -144,14 +145,16 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let eterm_obligations name nclen evm fs t tycon = 
+let eterm_obligations name nclen isevars evm fs t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
   let evl = List.rev (to_list evm) in
   let evn = 
     let i = ref (-1) in
       List.rev_map (fun (id, ev) -> incr i; 
-		  (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl
+		      (id, (!i, id_of_string
+			      (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
+		       ev)) evl
   in
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
@@ -171,7 +174,10 @@ let eterm_obligations name nclen evm fs t tycon =
 		 t, trunc_named_context fs hyps, fs
 	     | None -> evtyp, hyps, 0
 	 in
-	 let y' = (id, ((n, nstr), hyps, chop, evtyp, deps)) in
+	 let loc, k = evar_source id isevars in
+	 let opacity = match k with QuestionMark o -> o | _ -> true in
+	 let opaque = if not opacity || chop <> fs then None else Some chop in
+	 let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in
 	   y' :: l) 
       evn []
   in 
@@ -179,7 +185,7 @@ let eterm_obligations name nclen evm fs t tycon =
     subst_evar_constr evts 0 t 
   in
   let evars = 
-    List.map (fun (_, ((_, name), _, chop, typ, deps)) -> name, typ, chop = fs, deps) evts
+    List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts
   in
     (try
        trace (str "Term given to eterm" ++ spc () ++
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index a67020c52d..71fd766e35 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -18,9 +18,10 @@ val mkMetas : int -> constr list
 
 (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
 
-val eterm_obligations : identifier -> int -> evar_map -> int -> constr -> types option -> (* id, named context length, evars, number of
-											     function prototypes to try to clear from evars contexts *)
+(* id, named context length, evars, number of
+   function prototypes to try to clear from evars contexts, object and optional type *)
+val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> 
   (identifier * types * bool * Intset.t) array * constr
-    (* Obl. name, type as product, chopping of products flag, and dependencies as indexes into the array *)
+    (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index b697e93320..fc2da8f587 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -145,10 +145,28 @@ let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgo
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
   print_subgoals ()
-  (*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
+(*     if !pcoq <> None then (out_some !pcoq).start_proof () *)
 
 let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
 
+
+let assumption_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is assumed")
+
+let declare_assumption env isevars idl is_coe k bl c =
+  if not (Pfedit.refining ()) then 
+    let evm, c, typ = 
+      Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None 
+    in
+      List.iter (Command.declare_one_assumption is_coe k c) idl
+  else
+    errorlabstrm "Command.Assumption"
+	(str "Cannot declare an assumption while in proof editing mode.")
+
+let vernac_assumption env isevars kind l =
+  List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l
+
+
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
@@ -159,7 +177,7 @@ let subtac (loc, command) =
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
-    match command with
+  match command with
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
 		 ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
@@ -190,6 +208,8 @@ let subtac (loc, command) =
 	  start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
 
 
+      | VernacAssumption (stre,l) -> 
+	  vernac_assumption env isevars stre l
 
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index b7243374b2..72fd421893 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1762,7 +1762,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs arity =
 	       | l -> RApp (dummy_loc, bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> RApp (dummy_loc, branch, [ RHole (dummy_loc, Evd.QuestionMark) ])
+	     Some _ -> RApp (dummy_loc, branch, [ RHole (dummy_loc, Evd.QuestionMark true) ])
 	   | None -> branch
 	 in
 	   (* 	 let branch =  *)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 94f1bdec0a..09ed69fb4d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -286,7 +286,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
 		 [| argtyp ;
 		    wf_rel ;
-		    make_existential dummy_loc intern_before_env isevars wf_proof ;
+		    make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ;
 		    prop ;
 		    intern_body_lam |])
       | Some f ->
@@ -309,7 +309,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (*   in *)
   let evm = non_instanciated_map env isevars in
     (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
-  let evars, evars_def = Eterm.eterm_obligations recname nc_len evm 0 fullcoqc (Some fullctyp) in
+  let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in
     (*     (try trace (str "Generated obligations : "); *)
 (*        Array.iter *)
     (* 	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
@@ -392,7 +392,7 @@ let build_mutrec l boxed =
       and typ = 
 	Termops.it_mkNamedProd_or_LetIn typ rec_sign
       in
-      let evars, def = Eterm.eterm_obligations id nc_len evm recdefs def (Some typ) in
+      let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in
 	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 647c47b6ad..e83ee66585 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -151,5 +151,5 @@ let subtac_proof env isevars id l c tycon =
   let nc = named_context env in
   let nc_len = named_context_length nc in
   let evm, coqc, coqt = subtac_process env isevars id l c tycon in
-  let evars, def = Eterm.eterm_obligations id nc_len evm 0 coqc (Some coqt) in
+  let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in
     add_definition id def coqt evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 990ee115f6..c2132f61b5 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -495,13 +495,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast(loc,c,k,t) ->
+    | RCast(loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
 		let cj = pretype empty_tycon env isevars lvar c in
 		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
-	    | CastConv k ->
+	    | CastConv (k,t) ->
 		let tj = pretype_type empty_valcon env isevars lvar t in
 		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
 		  (* User Casts are for helping pretyping, experimentally not to be kept*)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 4dc157397a..2e362a2107 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -152,8 +152,8 @@ let app_opt c e =
 let print_args env args = 
   Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
 
-let make_existential loc env isevars c =
-  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
+let make_existential loc ?(opaque = true) env isevars c =
+  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
   let (key, args) = destEvar evar in
     (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
 		  print_args env args ++ str " for type: "++ 
@@ -169,7 +169,7 @@ let make_existential_expr loc env c =
 let string_of_hole_kind = function
   | ImplicitArg _ -> "ImplicitArg"
   | BinderType _ -> "BinderType"
-  | QuestionMark -> "QuestionMark"
+  | QuestionMark _ -> "QuestionMark"
   | CasesType -> "CasesType"
   | InternalHole -> "InternalHole"
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
@@ -182,7 +182,7 @@ let non_instanciated_map env evd =
 	   debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
 		      str (string_of_hole_kind k));
 	   match k with 
-	       QuestionMark -> Evd.add evm key evi
+	       QuestionMark _ -> Evd.add evm key evi
 	     | _ ->
 	       debug 2 (str " and is an implicit");
 	       Pretype_errors.error_unsolvable_implicit loc env evm k)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 00f01d6e1c..37ee1ac23a 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -82,7 +82,7 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t
 type binders = local_binder list
 val app_opt : ('a -> 'a) option -> 'a -> 'a
 val print_args : env -> constr array -> std_ppcmds
-val make_existential : loc -> env -> evar_defs ref -> types -> constr
+val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr
 val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 val string_of_hole_kind : hole_kind -> string
 val non_instanciated_map : env -> evar_defs ref -> evar_map