aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/eterm.ml46
-rw-r--r--contrib/subtac/eterm.mli11
-rw-r--r--contrib/subtac/subtac.ml16
-rw-r--r--contrib/subtac/subtac_cases.ml2
-rw-r--r--contrib/subtac/subtac_command.ml2
-rw-r--r--contrib/subtac/subtac_obligations.ml208
-rw-r--r--contrib/subtac/subtac_obligations.mli7
-rw-r--r--contrib/subtac/subtac_utils.ml3
-rw-r--r--contrib/subtac/subtac_utils.mli3
-rw-r--r--interp/constrintern.ml2
-rw-r--r--parsing/q_constr.ml42
-rw-r--r--pretyping/evd.ml4
-rw-r--r--pretyping/evd.mli7
-rw-r--r--tactics/decl_interp.ml2
14 files changed, 192 insertions, 123 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 037911a19..c2d7a59f1 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -6,6 +6,7 @@
*)
open Term
+open Sign
open Names
open Evd
open List
@@ -20,15 +21,26 @@ let trace s =
let succfix (depth, fixrels) =
(succ depth, List.map succ fixrels)
+type oblinfo =
+ { ev_name: int * identifier;
+ ev_hyps: named_context;
+ ev_status : obligation_definition_status;
+ ev_chop: int option;
+ ev_loc: Util.loc;
+ ev_typ: types;
+ ev_deps: Intset.t }
+
(** Substitute evar references in t using De Bruijn indices,
where n binders were passed through. *)
+
let subst_evar_constr evs n t =
let seen = ref Intset.empty in
let transparent = ref Idset.empty in
let evar_info id = List.assoc id evs in
let rec substrec (depth, fixrels) c = match kind_of_term c with
| Evar (k, args) ->
- let (id, idstr), hyps, chop, _, _, _ =
+ let { ev_name = (id, idstr) ;
+ ev_hyps = hyps ; ev_chop = chop } =
try evar_info k
with Not_found ->
anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
@@ -117,7 +129,7 @@ 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 env name isevars evm fs t ty =
+let eterm_obligations env name isevars evm fs ?status t ty =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
let nc = Environ.named_context env in
@@ -139,14 +151,22 @@ let eterm_obligations env name isevars evm fs t ty =
let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
let evtyp, hyps, chop =
match chop_product fs evtyp with
- Some t -> t, trunc_named_context fs hyps, fs
- | None -> evtyp, hyps, 0
+ | Some t -> t, trunc_named_context fs hyps, fs
+ | None -> evtyp, hyps, 0
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, loc, evtyp, deps)) in
- y' :: l)
+ let status = match k with QuestionMark o -> Some o | _ -> status in
+ let status, chop = match status with
+ | Some (Define true as stat) ->
+ if chop <> fs then Define false, None
+ else stat, Some chop
+ | Some s -> s, None
+ | None -> Define true, None
+ in
+ let info = { ev_name = (n, nstr);
+ ev_hyps = hyps; ev_status = status; ev_chop = chop;
+ ev_loc = loc; ev_typ = evtyp ; ev_deps = deps }
+ in (id, info) :: l)
evn []
in
let t', _, transparent = (* Substitute evar refs in the term by variables *)
@@ -154,8 +174,14 @@ let eterm_obligations env name isevars evm fs t ty =
in
let ty, _, _ = subst_evar_constr evts 0 ty in
let evars =
- List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) ->
- name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts
+ List.map (fun (_, info) ->
+ let { ev_name = (_, name); ev_status = status;
+ ev_loc = loc; ev_typ = typ; ev_deps = deps } = info
+ in
+ let status = match status with
+ | Define true when Idset.mem name transparent -> Define false
+ | _ -> status
+ in name, typ, loc, status, deps) evts
in Array.of_list (List.rev evars), t', ty
let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index bf854abb3..e197024ff 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -16,11 +16,12 @@ open Util
val mkMetas : int -> constr list
-(* env, id, evars, number of
- function prototypes to try to clear from evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types ->
- (identifier * types * loc * bool * Intset.t) array * constr * types
+(* env, id, evars, number of function prototypes to try to clear from
+ evars contexts, object and type *)
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int ->
+ ?status:obligation_definition_status -> constr -> types ->
+ (identifier * types * loc * obligation_definition_status * Intset.t) array * constr * types
(* Obl. name, type as product, location of the original evar,
- opacity (true = opaque) and dependencies as indexes into the array *)
+ status 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 baf565ab1..acf1ae838 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -52,16 +52,14 @@ open Tacexpr
let solve_tccs_in_type env id isevars evm c typ =
if not (evm = Evd.empty) then
let stmt_id = Nameops.add_suffix id "_stmt" in
- let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
- (** Make all obligations transparent so that real dependencies can be sorted out by the user *)
- let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
+ let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
match Subtac_obligations.add_definition stmt_id c' typ obls with
- Subtac_obligations.Defined cst -> constant_value (Global.env())
- (match cst with ConstRef kn -> kn | _ -> assert false)
- | _ ->
- errorlabstrm "start_proof"
- (str "The statement obligations could not be resolved automatically, " ++ spc () ++
- str "write a statement definition first.")
+ Subtac_obligations.Defined cst -> constant_value (Global.env())
+ (match cst with ConstRef kn -> kn | _ -> assert false)
+ | _ ->
+ errorlabstrm "start_proof"
+ (str "The statement obligations could not be resolved automatically, " ++ spc () ++
+ str "write a statement definition first.")
else
let _ = Typeops.infer_type env c in c
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 009b80606..f45efe50b 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1572,7 +1572,7 @@ let mk_JMeq typ x typ' y =
mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
-let hole = RHole (dummy_loc, Evd.QuestionMark true)
+let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
let context_of_arsign l =
let (x, _) = List.fold_right
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index a2f54b02d..503f34619 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -284,7 +284,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
mkApp (constr_of_global (Lazy.force fix_sub_ref),
[| argtyp ;
wf_rel ;
- make_existential dummy_loc ~opaque:false env isevars wf_proof ;
+ make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
lift lift_cst prop ;
lift lift_cst intern_body_lam |])
| Some f ->
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 563b228d8..6d1ec5ede 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,7 +1,9 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
open Printf
open Pp
open Subtac_utils
open Command
+open Environ
open Term
open Names
@@ -16,6 +18,7 @@ open Declare
type definition_hook = global_reference -> unit
+let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
@@ -25,14 +28,14 @@ let explain_no_obligations = function
Some ident -> str "No obligations for program " ++ str (string_of_id ident)
| None -> str "No obligations remaining"
-type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
+type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t) array
type obligation =
{ obl_name : identifier;
obl_type : types;
obl_location : loc;
obl_body : constr option;
- obl_opaque : bool;
+ obl_status : obligation_definition_status;
obl_deps : Intset.t;
}
@@ -79,22 +82,29 @@ let _ =
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
-let subst_deps obls deps t =
- Intset.fold
- (fun x acc ->
- let xobl = obls.(x) in
- debug 3 (str "Trying to get body of obligation " ++ int x);
- let oblb =
- try Option.get xobl.obl_body
- with _ ->
- debug 3 (str "Couldn't get body of obligation " ++ int x);
- assert(false)
- in
- Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
- deps t
-
+let get_obligation_body expand obl =
+ let c = Option.get obl.obl_body in
+ if expand && obl.obl_status = Expand then
+ match kind_of_term c with
+ | Const c -> constant_value (Global.env ()) c
+ | _ -> c
+ else c
+
+let subst_deps expand obls deps t =
+ let subst =
+ Intset.fold
+ (fun x acc ->
+ let xobl = obls.(x) in
+ let oblb =
+ try get_obligation_body expand xobl
+ with _ -> assert(false)
+ in (xobl.obl_name, oblb) :: acc)
+ deps []
+ in(* Termops.it_mkNamedProd_or_LetIn t subst *)
+ Term.replace_vars subst t
+
let subst_deps_obl obls obl =
- let t' = subst_deps obls obl.obl_deps obl.obl_type in
+ let t' = subst_deps false obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
@@ -150,14 +160,14 @@ let rec intset_to = function
-1 -> Intset.empty
| n -> Intset.add n (intset_to (pred n))
-let subst_body prg =
+let subst_body expand prg =
let obls, _ = prg.prg_obligations in
let ints = intset_to (pred (Array.length obls)) in
- subst_deps obls ints prg.prg_body,
- subst_deps obls ints (Termops.refresh_universes prg.prg_type)
+ subst_deps expand obls ints prg.prg_body,
+ subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
let declare_definition prg =
- let body, typ = subst_body prg in
+ let body, typ = subst_body false prg in
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
my_print_constr (Global.env()) body ++ str " : " ++
my_print_constr (Global.env()) prg.prg_type);
@@ -216,14 +226,18 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
list_map_i (fun i _ -> i) 0 ctx
+let reduce_fix =
+ Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+
let declare_mutual_definition l =
let len = List.length l in
let fixdefs, fixtypes, fiximps =
list_split3
(List.map (fun x ->
- let subs, typ = (subst_body x) in
+ let subs, typ = (subst_body false x) in
snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
in
+(* let fixdefs = List.map reduce_fix fixdefs in *)
let fixkind = Option.get (List.hd l).prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
@@ -248,18 +262,23 @@ let declare_mutual_definition l =
(match List.hd kns with ConstRef kn -> kn | _ -> assert false)
let declare_obligation obl body =
- let ce =
- { const_entry_body = body;
- const_entry_type = Some obl.obl_type;
- const_entry_opaque = if get_proofs_transparency () then false else obl.obl_opaque;
- const_entry_boxed = false}
- in
- let constant = Declare.declare_constant obl.obl_name
- (DefinitionEntry ce,IsProof Property)
- in
- print_message (Subtac_utils.definition_message obl.obl_name);
- { obl with obl_body = Some (mkConst constant) }
-
+ match obl.obl_status with
+ | Expand -> { obl with obl_body = Some body }
+ | Define opaque ->
+ let ce =
+ { const_entry_body = body;
+ const_entry_type = Some obl.obl_type;
+ const_entry_opaque =
+ (if get_proofs_transparency () then false
+ else opaque) ;
+ const_entry_boxed = false}
+ in
+ let constant = Declare.declare_constant obl.obl_name
+ (DefinitionEntry ce,IsProof Property)
+ in
+ print_message (Subtac_utils.definition_message obl.obl_name);
+ { obl with obl_body = Some (mkConst constant) }
+
let red = Reductionops.nf_betaiota
let init_prog_info n b t deps fixkind notations obls impls kind hook =
@@ -268,7 +287,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook =
(fun i (n, t, l, o, d) ->
debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
{ obl_name = n ; obl_body = None;
- obl_location = l; obl_type = red t; obl_opaque = o;
+ obl_location = l; obl_type = red t; obl_status = o;
obl_deps = d })
obls
in
@@ -356,22 +375,16 @@ let has_dependencies obls n =
!res
let kind_of_opacity o =
- if o then Subtac_utils.goal_proof_kind
- else Subtac_utils.goal_kind
-
-let obligations_of_evars evars =
- let arr =
- Array.of_list
- (List.map
- (fun (n, t) ->
- { obl_name = n;
- obl_type = t;
- obl_location = dummy_loc;
- obl_body = None;
- obl_opaque = false;
- obl_deps = Intset.empty;
- }) evars)
- in arr, Array.length arr
+ match o with
+ | Define false | Expand -> Subtac_utils.goal_kind
+ | _ -> Subtac_utils.goal_proof_kind
+
+let not_transp_msg =
+ str "Obligation should be transparent but was declared opaque." ++ spc () ++
+ str"Use 'Defined' instead."
+
+let warn_not_transp () = ppwarn not_transp_msg
+let error_not_transp () = pperror not_transp_msg
let rec solve_obligation prg num =
let user_num = succ num in
@@ -381,26 +394,37 @@ let rec solve_obligation prg num =
pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
else
match deps_remaining obls obl.obl_deps with
- [] ->
- let obl = subst_deps_obl obls obl in
- Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type
- (fun strength gr ->
- debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");
- let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
- let obls = Array.copy obls in
- let _ = obls.(num) <- obl in
- match update_obls prg obls (pred rem) with
- | Remain n when n > 0 ->
- if has_dependencies obls num then
- ignore(auto_solve_obligations (Some prg.prg_name))
- | _ -> ());
- trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
- Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
- Pfedit.by !default_tactic;
- Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
- | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
- ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
-
+ | [] ->
+ let obl = subst_deps_obl obls obl in
+ Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
+ (fun strength gr ->
+ let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+ let obl =
+ let transparent = evaluable_constant cst (Global.env ()) in
+ let body =
+ match obl.obl_status with
+ | Expand ->
+ if not transparent then error_not_transp ()
+ else constant_value (Global.env ()) cst
+ | Define opaque ->
+ if not opaque && not transparent then error_not_transp ()
+ else Libnames.constr_of_global gr
+ in { obl with obl_body = Some body }
+ in
+ let obls = Array.copy obls in
+ let _ = obls.(num) <- obl in
+ match update_obls prg obls (pred rem) with
+ | Remain n when n > 0 ->
+ if has_dependencies obls num then
+ ignore(auto_solve_obligations (Some prg.prg_name))
+ | _ -> ());
+ trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
+ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
+ Pfedit.by !default_tactic;
+ Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+ | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+ ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+
and subtac_obligation (user_num, name, typ) =
let num = pred user_num in
let prg = get_prog_err name in
@@ -422,11 +446,8 @@ and solve_obligation_by_tac prg obls i tac =
if deps_remaining obls obl.obl_deps = [] then
let obl = subst_deps_obl obls obl in
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
- if obl.obl_opaque then
- obls.(i) <- declare_obligation obl t
- else
- obls.(i) <- { obl with obl_body = Some t };
- true
+ obls.(i) <- declare_obligation obl t;
+ true
else false
with
| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
@@ -473,21 +494,25 @@ let show_obligations ?(msg=true) n =
let prg = get_prog_err n in
let n = prg.prg_name in
let obls, rem = prg.prg_obligations in
+ let showed = ref 5 in
if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
Array.iteri (fun i x ->
match x.obl_body with
- None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
- my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
- | Some _ -> ())
+ | None ->
+ if !showed > 0 then (
+ decr showed;
+ msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
+ hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
+ | Some _ -> ())
obls
-
+
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
let prg = init_prog_info n b t [] None [] obls implicits kind hook in
let obls,_ = prg.prg_obligations in
@@ -500,12 +525,16 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=
let len = Array.length obls in
let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
from_prg := ProgMap.add n prg !from_prg;
- let res = auto_solve_obligations (Some n) in
+ let res =
+ match tactic with
+ | None -> auto_solve_obligations (Some n)
+ | Some tac -> solve_obligations (Some n) tac
+ in
match res with
- | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
- | _ -> res)
+ | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+ | _ -> res)
-let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, imps, obls) ->
@@ -518,8 +547,13 @@ let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
List.fold_left (fun finished x ->
if finished then finished
else
- match auto_solve_obligations (Some x) with
- Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
+ let res =
+ match tactic with
+ | None -> auto_solve_obligations (Some x)
+ | Some tac -> solve_obligations (Some x) tac
+ in
+ match res with
+ | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
| _ -> false)
false deps
in ()
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 6d13e3bd3..355ca7cd7 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,9 +1,10 @@
open Names
open Util
open Libnames
+open Evd
-type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
- (* ident, type, location, opaque or transparent, dependencies *)
+type obligation_info = (identifier * Term.types * loc * obligation_definition_status * Intset.t) array
+ (* ident, type, location, opaque or transparent, expand or define dependencies *)
type progress = (* Resolution status of a program *)
| Remain of int (* n obligations remaining *)
@@ -21,6 +22,7 @@ type definition_hook = global_reference -> unit
val add_definition : Names.identifier -> Term.constr -> Term.types ->
?implicits:(Topconstr.explicitation * (bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
+ ?tactic:Proof_type.tactic ->
?hook:definition_hook -> obligation_info -> progress
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -28,6 +30,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option)
val add_mutual_definitions :
(Names.identifier * Term.constr * Term.types *
(Topconstr.explicitation * (bool * bool)) list * obligation_info) list ->
+ ?tactic:Proof_type.tactic ->
?kind:Decl_kinds.definition_kind ->
notations ->
Command.fixpoint_kind -> unit
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index bae2731aa..920b33b7a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -159,7 +159,7 @@ 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 ?(opaque = true) env isevars c =
+let make_existential loc ?(opaque = Define 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: " ++
@@ -470,4 +470,3 @@ let tactics_tac s =
let tactics_call tac args =
TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
-
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 493352114..964f668f2 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -83,7 +83,8 @@ 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 -> ?opaque:bool -> env -> evar_defs ref -> types -> constr
+val make_existential : loc -> ?opaque:obligation_definition_status ->
+ env -> evar_defs ref -> types -> constr
val make_existential_expr : loc -> 'a -> 'b -> constr_expr
val string_of_hole_kind : hole_kind -> string
val evars_of_term : evar_map -> evar_map -> constr -> evar_map
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 26ed02379..be7c75663 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -940,7 +940,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let p' = Option.map (intern_type env'') po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole (loc, k) ->
- RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
+ RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
| CPatVar (loc, n) when allow_patvar ->
RPatVar (loc, n)
| CPatVar (loc, _) ->
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 44ca8eb2c..a796cef82 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -75,7 +75,7 @@ EXTEND
| "0"
[ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >>
| id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >>
- | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >>
+ | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark (Define False)) >>
| "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >>
| "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 270dac01a..b29afc0cb 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -400,10 +400,12 @@ let metamap_to_list m =
(*************************)
(* Unification state *)
+type obligation_definition_status = Define of bool | Expand
+
type hole_kind =
| ImplicitArg of global_reference * (int * identifier option)
| BinderType of name
- | QuestionMark of bool
+ | QuestionMark of obligation_definition_status
| CasesType
| InternalHole
| TomatchTypeParameter of inductive * int
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cb7429002..38db90dad 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -166,11 +166,16 @@ val empty_evar_defs : evar_defs
val evars_of : evar_defs -> evar_map
val evars_reset_evd : evar_map -> evar_defs -> evar_defs
+(* Should the obligation be defined (opaque or transparent (default)) or
+ defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
(* Evars *)
type hole_kind =
| ImplicitArg of global_reference * (int * identifier option)
| BinderType of name
- | QuestionMark of bool (* Can it be turned into an obligation ? *)
+ | QuestionMark of obligation_definition_status
| CasesType
| InternalHole
| TomatchTypeParameter of inductive * int
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index a25fcd923..2be95056e 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -342,7 +342,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
(fun (loc,(id,_)) ->
RVar (loc,id)) params in
let dum_args=
- list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark false))
+ list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define false)))
oib.Declarations.mind_nrealargs in
raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
let pat_vars,aliases,patt = interp_pattern env pat in
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 14:10:33 +0000