summaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/eterm.ml19
-rw-r--r--plugins/subtac/eterm.mli3
-rw-r--r--plugins/subtac/g_subtac.ml416
-rw-r--r--plugins/subtac/subtac.ml28
-rw-r--r--plugins/subtac/subtac_cases.ml51
-rw-r--r--plugins/subtac/subtac_cases.mli6
-rw-r--r--plugins/subtac/subtac_classes.ml39
-rw-r--r--plugins/subtac/subtac_classes.mli6
-rw-r--r--plugins/subtac/subtac_coercion.ml21
-rw-r--r--plugins/subtac/subtac_command.ml64
-rw-r--r--plugins/subtac/subtac_command.mli8
-rw-r--r--plugins/subtac/subtac_obligations.ml171
-rw-r--r--plugins/subtac/subtac_obligations.mli2
-rw-r--r--plugins/subtac/subtac_pretyping.ml19
-rw-r--r--plugins/subtac/subtac_pretyping.mli2
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml167
-rw-r--r--plugins/subtac/subtac_utils.ml44
-rw-r--r--plugins/subtac/subtac_utils.mli14
18 files changed, 353 insertions, 327 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 3fb6824b..5ed335d0 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(**
- Get types of existentials ;
- Flatten dependency tree (prefix order) ;
@@ -28,11 +27,15 @@ type oblinfo =
ev_hyps: named_context;
ev_status: obligation_definition_status;
ev_chop: int option;
- ev_source: hole_kind located;
+ ev_src: hole_kind located;
ev_typ: types;
ev_tac: tactic option;
ev_deps: Intset.t }
+(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
+open Store.Field
+let evar_tactic = Store.field ()
+
(** Substitute evar references in t using De Bruijn indices,
where n binders were passed through. *)
@@ -210,7 +213,7 @@ let eterm_obligations env name isevars evm fs ?status t ty =
| Some s -> s, None
| None -> Define true, None
in
- let tac = match ev.evar_extra with
+ let tac = match evar_tactic.get ev.evar_extra with
| Some t ->
if Dyn.tag t = "tactic" then
Some (Tacinterp.interp
@@ -218,9 +221,9 @@ let eterm_obligations env name isevars evm fs ?status t ty =
else None
| None -> None
in
- let info = { ev_name = (n, nstr); ev_hyps = hyps;
- ev_status = status; ev_chop = chop;
- ev_source = (loc, k); ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
+ let info = { ev_name = (n, nstr);
+ ev_hyps = hyps; ev_status = status; ev_chop = chop;
+ ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
in (id, info) :: l)
evn []
in
@@ -231,12 +234,12 @@ let eterm_obligations env name isevars evm fs ?status t ty =
let evars =
List.map (fun (ev, info) ->
let { ev_name = (_, name); ev_status = status;
- ev_source = source; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+ ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
in
let status = match status with
| Define true when Idset.mem name transparent -> Define false
| _ -> status
- in name, typ, source, status, deps, tac) evts
+ in name, typ, src, status, deps, tac) evts
in
let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index b4bbe3d5..03d76f29 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: eterm.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Environ
open Tacmach
open Term
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index ce6d12be..ca1240e5 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -1,21 +1,17 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
-
(*
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-(* $Id: g_subtac.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Flags
open Util
@@ -37,14 +33,14 @@ module Tactic = Pcoq.Tactic
module SubtacGram =
struct
- let gec s = Gram.Entry.create ("Subtac."^s)
+ let gec s = Gram.entry_create ("Subtac."^s)
(* types *)
- let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
+ let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc"
- let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.Entry.e = gec "subtac_withtac"
+ let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac"
end
-open Rawterm
+open Glob_term
open SubtacGram
open Util
open Pcoq
@@ -94,7 +90,7 @@ VERNAC COMMAND EXTEND Subtac
let try_catch_exn f e =
try f e
- with exn -> errorlabstrm "Program" (Cerrors.explain_exn exn)
+ with exn -> errorlabstrm "Program" (Errors.print exn)
let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 95cacc38..710149ae 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -1,13 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
+open Compat
open Global
open Pp
open Util
@@ -27,7 +26,7 @@ open List
open Recordops
open Evarutil
open Pretype_errors
-open Rawterm
+open Glob_term
open Evarconv
open Pattern
open Vernacexpr
@@ -50,7 +49,7 @@ open Tacinterp
open Tacexpr
let solve_tccs_in_type env id isevars evm c typ =
- if not (evm = Evd.empty) then
+ if not (Evd.is_empty evm) then
let stmt_id = Nameops.add_suffix id "_stmt" 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 ~term:c' typ obls with
@@ -89,7 +88,7 @@ let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
print_subgoals ()
-let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
+let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
@@ -142,12 +141,12 @@ let subtac (loc, command) =
(fun _ _ -> ())
| DefineBody (bl, _, c, tycon) ->
ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
- | VernacFixpoint (l, b) ->
+ | VernacFixpoint l ->
List.iter (fun ((lid, _, _, _, _), _) ->
check_fresh lid;
Dumpglob.dump_definition lid false "fix") l;
let _ = trace (str "Building fixpoint") in
- ignore(Subtac_command.build_recursive l b)
+ ignore(Subtac_command.build_recursive l)
| VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
if guard <> None then
@@ -172,10 +171,10 @@ let subtac (loc, command) =
error "Declare Instance not supported here.";
ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
- | VernacCoFixpoint (l, b) ->
+ | VernacCoFixpoint l ->
if Dumpglob.dump () then
List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
- ignore(Subtac_command.build_corecursive l b)
+ ignore(Subtac_command.build_corecursive l)
(*| VernacEndProof e ->
subtac_end_proof e*)
@@ -219,6 +218,11 @@ let subtac (loc, command) =
| Type_errors.TypeError (env, exn) as e -> raise e
- | Pretype_errors.PretypeError (env, exn) as e -> raise e
+ | Pretype_errors.PretypeError (env, _, exn) as e -> raise e
+
+ | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+ Loc.Exc_located (loc, e') as e) -> raise e
- | e -> raise e
+ | e ->
+ (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
+ raise e
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 25aec39c..368d8bac 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_cases.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Cases
open Util
open Names
@@ -23,7 +20,7 @@ open Sign
open Reductionops
open Typeops
open Type_errors
-open Rawterm
+open Glob_term
open Retyping
open Pretype_errors
open Evarutil
@@ -89,7 +86,7 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
type rhs =
{ rhs_env : env;
avoid_ids : identifier list;
- it : rawconstr;
+ it : glob_constr;
}
type equation =
@@ -158,22 +155,22 @@ let feed_history arg = function
(* This is for non exhaustive error message *)
-let rec rawpattern_of_partial_history args2 = function
+let rec glob_pattern_of_partial_history args2 = function
| Continuation (n, args1, h) ->
let args3 = make_anonymous_patvars (n - (List.length args2)) in
- build_rawpattern (List.rev_append args1 (args2@args3)) h
+ build_glob_pattern (List.rev_append args1 (args2@args3)) h
| Result pl -> pl
-and build_rawpattern args = function
+and build_glob_pattern args = function
| Top -> args
| MakeAlias (AliasLeaf, rh) ->
assert (args = []);
- rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
+ glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
| MakeAlias (AliasConstructor pci, rh) ->
- rawpattern_of_partial_history
+ glob_pattern_of_partial_history
[PatCstr (dummy_loc, pci, args, Anonymous)] rh
-let complete_history = rawpattern_of_partial_history []
+let complete_history = glob_pattern_of_partial_history []
(* This is to build glued pattern-matching history and alias bodies *)
@@ -237,7 +234,7 @@ type pattern_matching_problem =
mat : matrix;
caseloc : loc;
casestyle: case_style;
- typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
+ typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment }
(*--------------------------------------------------------------------------*
* A few functions to infer the inductive type from the patterns instead of *
@@ -369,10 +366,10 @@ let find_tomatch_tycon isevars env loc = function
| None -> empty_tycon
let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
- let loc = Some (loc_of_rawconstr tomatch) in
+ let loc = Some (loc_of_glob_constr tomatch) in
let tycon = find_tomatch_tycon isevars env loc indopt in
let j = typing_fun tycon env tomatch in
- let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
+ let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in
isevars := evd;
let typ = nf_evar ( !isevars) j.uj_type in
let t =
@@ -530,7 +527,7 @@ let extract_rhs pb =
let occur_in_rhs na rhs =
match na with
| Anonymous -> false
- | Name id -> occur_rawconstr id rhs.it
+ | Name id -> occur_glob_constr id rhs.it
let is_dep_patt eqn = function
| PatVar (_,name) -> occur_in_rhs name eqn.rhs
@@ -604,7 +601,7 @@ let regeneralize_index_tomatch n =
genrec 0
let rec replace_term n c k t =
- if t = mkRel (n+k) then lift k c
+ if isRel t && destRel t = n+k then lift k c
else map_constr_with_binders succ (replace_term n c) k t
let replace_tomatch n c =
@@ -1518,7 +1515,7 @@ let mk_JMeq typ x typ' y =
mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |])
-let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
+let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
let constr_of_pat env isevars arsign pat avoid =
let rec typ env (ty, realargs) pat avoid =
@@ -1534,7 +1531,7 @@ let constr_of_pat env isevars arsign pat avoid =
| PatCstr (l,((_, i) as cstr),args,alias) ->
let cind = inductive_of_constructor cstr in
let IndType (indf, _) =
- try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty)
+ try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty)
with Not_found -> error_case_not_inductive env
{uj_val = ty; uj_type = Typing.type_of env !isevars ty}
in
@@ -1548,7 +1545,7 @@ let constr_of_pat env isevars arsign pat avoid =
List.fold_right2
(fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) ->
let pat', sign', arg', typ', argtypargs, n', avoid =
- typ env (lift (n - m) t, []) ua avoid
+ typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid
in
let args' = arg' :: List.map (lift n') args in
let env' = push_rels sign' env in
@@ -1607,12 +1604,12 @@ let vars_of_ctx ctx =
match b with
| Some t' when kind_of_term t' = Rel 0 ->
prev,
- (RApp (dummy_loc,
- (RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+ (GApp (dummy_loc,
+ (GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars
| _ ->
match na with
Anonymous -> raise (Invalid_argument "vars_of_ctx")
- | Name n -> n, RVar (dummy_loc, n) :: vars)
+ | Name n -> n, GVar (dummy_loc, n) :: vars)
ctx (id_of_string "vars_of_ctx_error", [])
in List.rev y
@@ -1744,13 +1741,13 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
let branch =
- let bref = RVar (dummy_loc, branch_name) in
+ let bref = GVar (dummy_loc, branch_name) in
match vars_of_ctx rhs_rels with
[] -> bref
- | l -> RApp (dummy_loc, bref, l)
+ | l -> GApp (dummy_loc, bref, l)
in
let branch = match ineqs with
- Some _ -> RApp (dummy_loc, branch, [ hole ])
+ Some _ -> GApp (dummy_loc, branch, [ hole ])
| None -> branch
in
incr i;
@@ -1786,7 +1783,7 @@ let abstract_tomatch env tomatchs tycon =
Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon
| _ ->
let tycon = Option.map
- (fun t -> subst_term_occ all_occurrences (lift 1 c) (lift 1 t)) tycon in
+ (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in
let name = next_ident_away (id_of_string "filtered_var") names in
(mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
(Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index bc2b2bb7..77537d33 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_cases.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*i*)
open Util
open Names
@@ -15,7 +13,7 @@ open Term
open Evd
open Environ
open Inductiveops
-open Rawterm
+open Glob_term
open Evarutil
(*i*)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 960bf162..c08dd16d 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -1,19 +1,16 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Pretyping
open Evd
open Environ
open Term
-open Rawterm
+open Glob_term
open Topconstr
open Names
open Libnames
@@ -23,24 +20,28 @@ open Constrintern
open Subtac_command
open Typeclasses
open Typeclasses_errors
-open Termops
open Decl_kinds
open Entries
open Util
module SPretyping = Subtac_pretyping.Pretyping
-let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
+let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c =
SPretyping.understand_tcc_evars evdref env kind
- (intern_gen (kind=IsType) ~impls ( !evdref) env c)
+ (intern_gen (kind=IsType) ~impls !evdref env c)
-let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
+let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
let interp_context_evars evdref env params =
- Constrintern.interp_context_gen
+ let impls_env, bl = Constrintern.interp_context_gen
(fun env t -> SPretyping.understand_tcc_evars evdref env IsType t)
- (SPretyping.understand_judgment_tcc evdref) !evdref env params
+ (SPretyping.understand_judgment_tcc evdref) !evdref env params in bl
+
+let interp_type_evars_impls ~evdref ?(impls=empty_internalization_env) env c =
+ let c = intern_gen true ~impls !evdref env c in
+ let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
+ SPretyping.understand_tcc_evars ~fail_evar:false evdref env IsType c, imps
let type_ctx_instance evars env ctx inst subst =
let rec aux (subst, instctx) l = function
@@ -113,11 +114,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let subst = List.map (Evarutil.nf_evar sigma) subst in
let props =
match props with
- | CRecord (loc, _, fs) ->
+ | Some (CRecord (loc, _, fs)) ->
if List.length fs > List.length k.cl_props then
Classes.mismatched_props env' (List.map snd fs) k.cl_props;
Inl fs
- | _ -> Inr props
+ | Some p -> Inr p
+ | None -> Inl []
in
let subst =
match props with
@@ -138,7 +140,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
let (loc, mid) = get_id loc_mid in
- Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+ List.iter
+ (fun (n, _, x) ->
+ if n = Name mid then
+ Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
+ k.cl_projs;
c :: props, rest'
with Not_found ->
(CHole (Util.dummy_loc, None) :: props), rest
@@ -173,10 +179,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
Evarutil.check_evars env Evd.empty !evars termtype;
let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
Impargs.declare_manual_implicits false gr ~enriching:false [imps];
- Typeclasses.add_instance inst
+ Typeclasses.declare_instance pri (not global) (ConstRef cst)
in
let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in
- id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
+ id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 73ca5581..5b5c0203 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*i*)
open Names
open Decl_kinds
@@ -35,7 +33,7 @@ val new_instance :
?global:bool ->
local_binder list ->
typeclass_constraint ->
- constr_expr ->
+ constr_expr option ->
?generalize:bool ->
int option ->
identifier * Subtac_obligations.progress
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index bdebdf85..74f31a90 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -1,13 +1,10 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_coercion.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Names
open Term
@@ -144,7 +141,7 @@ module Coercion = struct
let restargs = lift_args 1
(List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
in
- let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
+ let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in
let evar = make_existential loc env isevars eq in
@@ -205,7 +202,7 @@ module Coercion = struct
| Lambda (n, t, t') -> c, t'
(*| Prod (n, t, t') -> t'*)
| Evar (k, args) ->
- let (evs, t) = Evarutil.define_evar_as_lambda !isevars (k,args) in
+ let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in
isevars := evs;
let (n, dom, rng) = destLambda t in
let (domk, args) = destEvar dom in
@@ -330,8 +327,8 @@ module Coercion = struct
let apply_pattern_coercion loc pat p =
List.fold_left
(fun pat (co,n) ->
- let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in
- Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+ let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
+ Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
pat p
(* raise Not_found if no coercion found *)
@@ -411,10 +408,10 @@ module Coercion = struct
else
let v', t' =
try
- let t2,t1,p = lookup_path_between env ( evd) (t,c1) in
+ let t2,t1,p = lookup_path_between env evd (t,c1) in
match v with
Some v ->
- let j = apply_coercion env ( evd) p
+ let j = apply_coercion env evd p
{uj_val = v; uj_type = t} t2 in
Some j.uj_val, j.uj_type
| None -> None, t
@@ -430,8 +427,8 @@ module Coercion = struct
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
- kind_of_term (whd_betadeltaiota env ( evd) t),
- kind_of_term (whd_betadeltaiota env ( evd) c1)
+ kind_of_term (whd_betadeltaiota env evd t),
+ kind_of_term (whd_betadeltaiota env evd c1)
with
| Prod (name,t1,t2), Prod (_,u1,u2) ->
(* Conversion did not work, we may succeed with a coercion. *)
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index a83611a4..ecae6759 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -6,7 +6,7 @@ open Libobject
open Pattern
open Matching
open Pp
-open Rawterm
+open Glob_term
open Sign
open Tacred
open Util
@@ -21,7 +21,6 @@ open Tacmach
open Tactic_debug
open Topconstr
open Term
-open Termops
open Tacexpr
open Safe_typing
open Typing
@@ -53,7 +52,7 @@ let evar_nf isevars c =
Evarutil.nf_evar !isevars c
let interp_gen kind isevars env
- ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+ ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
let c' = SPretyping.understand_tcc_evars isevars env kind c' in
@@ -62,13 +61,13 @@ let interp_gen kind isevars env
let interp_constr isevars env c =
interp_gen (OfType None) isevars env c
-let interp_type_evars isevars env ?(impls=[]) c =
+let interp_type_evars isevars env ?(impls=Constrintern.empty_internalization_env) c =
interp_gen IsType isevars env ~impls c
-let interp_casted_constr isevars env ?(impls=[]) c typ =
+let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
-let interp_casted_constr_evars isevars env ?(impls=[]) c typ =
+let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
let interp_open_constr isevars env c =
@@ -85,25 +84,25 @@ let interp_constr_judgment isevars env c =
{ uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
let locate_if_isevar loc na = function
- | RHole _ ->
+ | GHole _ ->
(try match na with
- | Name id -> Reserve.find_reserved_type id
+ | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
| Anonymous -> raise Not_found
- with Not_found -> RHole (loc, Evd.BinderType na))
+ with Not_found -> GHole (loc, Evd.BinderType na))
| x -> x
let interp_binder sigma env na t =
let t = Constrintern.intern_gen true ( !sigma) env t in
- SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+ SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t)
let interp_context_evars evdref env params =
- let bl = Constrintern.intern_context false ( !evdref) env params in
+ let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_env params in
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
match b with
None ->
- let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t' = locate_if_isevar (loc_of_glob_constr t) na t in
let t = SPretyping.understand_tcc_evars evdref env IsType t' in
let d = (na,None,t) in
let impls =
@@ -133,7 +132,7 @@ let collect_non_rec env =
let i =
list_try_find_i
(fun i f ->
- if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+ if List.for_all (fun (_, def) -> not (Termops.occur_var env f def)) ldefrec
then i else failwith "try_find_i")
0 lnamerec
in
@@ -184,11 +183,11 @@ let sigT = Lazy.lazy_from_fun build_sigma_type
let sigT_info = lazy
{ ci_ind = destInd (Lazy.force sigT).typ;
ci_npar = 2;
- ci_cstr_nargs = [|2|];
+ ci_cstr_ndecls = [|2|];
ci_pp_info = { ind_nargs = 0; style = LetStyle }
}
-let telescope = function
+let rec telescope = function
| [] -> assert false
| [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
| (n, None, t) :: tl ->
@@ -209,13 +208,14 @@ let telescope = function
(List.rev tys) tl (mkRel 1, [])
in ty, ((n, Some last, t) :: subst), constr
- | _ -> raise (Invalid_argument "telescope")
+ | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in
+ ty, ((n, Some b, t) :: subst), lift 1 term
let nf_evar_context isevars ctx =
List.map (fun (n, b, t) ->
(n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx
-let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
+let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
Coqlib.check_required_library ["Coq";"Program";"Wf"];
let sigma = Evd.empty in
let isevars = ref (Evd.create_evar_defs sigma) in
@@ -300,11 +300,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
Constrintern.compute_internalization_data env
Constrintern.Recursive full_arity impls
in
- let newimpls = [(recname, (r, l, impls @
- [Some (id_of_string "recproof", Impargs.Manual, (true, false))],
- scopes @ [None]))] in
- interp_casted_constr isevars ~impls:newimpls
- (push_rel_context ctx env) body (lift 1 top_arity)
+ let newimpls = Idmap.singleton recname
+ (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))],
+ scopes @ [None]) in
+ interp_casted_constr isevars ~impls:newimpls
+ (push_rel_context ctx env) body (lift 1 top_arity)
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
@@ -325,10 +325,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ce =
- { const_entry_body = Evarutil.nf_evar !isevars body;
+ { const_entry_body = Evarutil.nf_evar !isevars body;
+ const_entry_secctx = None;
const_entry_type = Some ty;
- const_entry_opaque = false;
- const_entry_boxed = false}
+ const_entry_opaque = false }
in
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
@@ -417,7 +417,7 @@ let out_def = function
| Some def -> def
| None -> error "Program Fixpoint needs defined bodies."
-let interp_recursive fixkind l boxed =
+let interp_recursive fixkind l =
let env = Global.env() in
let fixl, ntnl = List.split l in
let kind = fixkind <> IsCoFixpoint in
@@ -506,7 +506,7 @@ let out_n = function
Some n -> n
| None -> raise Not_found
-let build_recursive l b =
+let build_recursive l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
@@ -514,24 +514,24 @@ let build_recursive l b =
(match n with Some n -> mkIdentC (snd n) | None ->
errorlabstrm "Subtac_command.build_recursive"
(str "Recursive argument required for well-founded fixpoints"))
- ntn false)
+ ntn)
| [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
- m ntn false)
+ m ntn)
| _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
Command.fix_body = def; Command.fix_type = typ},ntn)) l
- in interp_recursive (IsFixpoint g) fixl b
+ in interp_recursive (IsFixpoint g) fixl
| _, _ ->
errorlabstrm "Subtac_command.build_recursive"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let build_corecursive l b =
+let build_corecursive l =
let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
Command.fix_body = def; Command.fix_type = typ},ntn))
l in
- interp_recursive IsCoFixpoint fixl b
+ interp_recursive IsCoFixpoint fixl
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 0f24915e..72549a01 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -43,7 +43,7 @@ val interp_binder : Evd.evar_map ref ->
val telescope :
- (Names.name * 'a option * Term.types) list ->
+ (Names.name * Term.types option * Term.types) list ->
Term.types * (Names.name * Term.types option * Term.types) list *
Term.constr
@@ -51,10 +51,10 @@ val build_wellfounded :
Names.identifier * 'a * Topconstr.local_binder list *
Topconstr.constr_expr * Topconstr.constr_expr ->
Topconstr.constr_expr ->
- Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
+ Topconstr.constr_expr -> 'b -> Subtac_obligations.progress
val build_recursive :
- (fixpoint_expr * decl_notation list) list -> bool -> unit
+ (fixpoint_expr * decl_notation list) list -> unit
val build_corecursive :
- (cofixpoint_expr * decl_notation list) list -> bool -> unit
+ (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index d3a63410..64d9f72c 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
open Printf
open Pp
open Subtac_utils
@@ -16,6 +15,7 @@ open Util
open Evd
open Declare
open Proof_type
+open Compat
let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Util.errorlabstrm "Program" cmd
@@ -30,13 +30,13 @@ 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 * hole_kind located *
+type obligation_info = (Names.identifier * Term.types * hole_kind located *
obligation_definition_status * Intset.t * tactic option) array
type obligation =
{ obl_name : identifier;
obl_type : types;
- obl_source : hole_kind located;
+ obl_location : hole_kind located;
obl_body : constr option;
obl_status : obligation_definition_status;
obl_deps : Intset.t;
@@ -82,11 +82,29 @@ open Goptions
let _ =
declare_bool_option
{ optsync = true;
+ optdepr = false;
optname = "transparency of Program obligations";
optkey = ["Transparent";"Obligations"];
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
+(* true = hide obligations *)
+let hide_obligations = ref false
+
+let set_hide_obligations = (:=) hide_obligations
+let get_hide_obligations () = !hide_obligations
+
+open Goptions
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "Hidding of Program obligations";
+ optkey = ["Hide";"Obligations"];
+ optread = get_hide_obligations;
+ optwrite = set_hide_obligations; }
+
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
let get_obligation_body expand obl =
@@ -97,18 +115,54 @@ let get_obligation_body expand obl =
| _ -> c
else c
+let obl_substitution expand obls deps =
+ 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, (xobl.obl_type, oblb)) :: acc)
+ deps []
+
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 = obl_substitution expand obls deps in
+ Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t
+
+let rec prod_app t n =
+ match kind_of_term (strip_outer_cast t) with
+ | Prod (_,_,b) -> subst1 n b
+ | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
+ | _ ->
+ errorlabstrm "prod_app"
+ (str"Needed a product, but didn't find one" ++ fnl ())
+
+
+(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_applist t nL = List.fold_left prod_app t nL
+
+let replace_appvars subst =
+ let rec aux c =
+ let f, l = decompose_app c in
+ if isVar f then
+ try
+ let c' = List.map (map_constr aux) l in
+ let (t, b) = List.assoc (destVar f) subst in
+ mkApp (delayed_force hide_obligation,
+ [| prod_applist t c'; applistc b c' |])
+ with Not_found -> map_constr aux c
+ else map_constr aux c
+ in map_constr aux
+
+let subst_prog expand obls ints prg =
+ let subst = obl_substitution expand obls ints in
+ if get_hide_obligations () then
+ (replace_appvars subst prg.prg_body,
+ replace_appvars subst (Termops.refresh_universes prg.prg_type))
+ else
+ let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
+ (Term.replace_vars subst' prg.prg_body,
+ Term.replace_vars subst' (Termops.refresh_universes prg.prg_type))
let subst_deps_obl obls obl =
let t' = subst_deps true obls obl.obl_deps obl.obl_type in
@@ -153,20 +207,32 @@ let _ =
let progmap_union = ProgMap.fold ProgMap.add
-let (input,output) =
+let close sec =
+ if not (ProgMap.is_empty !from_prg) then
+ let keys = map_keys !from_prg in
+ errorlabstrm "Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
+ prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
+ (str (if List.length keys = 1 then " has " else "have ") ++
+ str "unsolved obligations"))
+
+let input : program_info ProgMap.t -> obj =
declare_object
{ (default_object "Program state") with
- classify_function = (fun () ->
- if not (ProgMap.is_empty !from_prg) then
- errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
- prlist_with_sep spc (fun x -> Nameops.pr_id x)
- (map_keys !from_prg));
- Dispose) }
+ cache_function = (fun (na, pi) -> from_prg := pi);
+ load_function = (fun _ (_, pi) -> from_prg := pi);
+ discharge_function = (fun _ -> close "section"; None);
+ classify_function = (fun _ -> close "module"; Dispose) }
open Evd
let progmap_remove prg =
- from_prg := ProgMap.remove prg.prg_name !from_prg
+ Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
+
+let progmap_add n prg =
+ Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
+
+let progmap_replace prg' =
+ Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
let rec intset_to = function
-1 -> Intset.empty
@@ -175,21 +241,16 @@ let rec intset_to = function
let subst_body expand prg =
let obls, _ = prg.prg_obligations in
let ints = intset_to (pred (Array.length obls)) in
- subst_deps expand obls ints prg.prg_body,
- subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
+ subst_prog expand obls ints prg
let declare_definition prg =
let body, typ = subst_body true 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);
- with _ -> ());
- let (local, boxed, kind) = prg.prg_kind in
+ let (local, kind) = prg.prg_kind in
let ce =
{ const_entry_body = body;
+ const_entry_secctx = None;
const_entry_type = Some typ;
- const_entry_opaque = false;
- const_entry_boxed = boxed}
+ const_entry_opaque = false }
in
(Command.get_declare_definition_hook ()) ce;
match local with
@@ -207,7 +268,7 @@ let declare_definition prg =
| (Global|Local) ->
let c =
Declare.declare_constant
- prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
+ prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind))
in
let gr = ConstRef c in
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
@@ -255,7 +316,7 @@ let declare_mutual_definition l =
let fixkind = Option.get first.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
- let (local,boxed,kind) = first.prg_kind in
+ let (local,kind) = first.prg_kind in
let fixnames = first.prg_deps in
let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
@@ -269,7 +330,7 @@ let declare_mutual_definition l =
None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
in
(* Declare the recursive definitions *)
- let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
+ let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation first.prg_notations;
Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
@@ -287,9 +348,9 @@ let declare_obligation prg obl body =
let opaque = if get_proofs_transparency () then false else opaque in
let ce =
{ const_entry_body = body;
+ const_entry_secctx = None;
const_entry_type = Some ty;
- const_entry_opaque = opaque;
- const_entry_boxed = false}
+ const_entry_opaque = opaque }
in
let constant = Declare.declare_constant obl.obl_name
(DefinitionEntry ce,IsProof Property)
@@ -307,14 +368,14 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
assert(obls = [||]);
let n = Nameops.add_suffix n "_obligation" in
[| { obl_name = n; obl_body = None;
- obl_source = (dummy_loc, QuestionMark Expand); obl_type = t;
+ obl_location = dummy_loc, InternalHole; obl_type = t;
obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
mkVar n
| Some b ->
Array.mapi
(fun i (n, t, l, o, d, tac) ->
{ obl_name = n ; obl_body = None;
- obl_source = l; obl_type = reduce t; obl_status = o;
+ obl_location = l; obl_type = reduce t; obl_status = o;
obl_deps = d; obl_tac = tac })
obls, b
in
@@ -359,7 +420,7 @@ let obligations_message rem =
let update_obls prg obls rem =
let prg' = { prg with prg_obligations = (obls, rem) } in
- from_prg := map_replace prg.prg_name prg' !from_prg;
+ progmap_replace prg';
obligations_message rem;
if rem > 0 then Remain rem
else (
@@ -437,7 +498,7 @@ let rec solve_obligation prg num tac =
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
let res = try update_obls prg obls (pred rem)
- with e -> pperror (Cerrors.explain_exn e)
+ with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
in
match res with
| Remain n when n > 0 ->
@@ -485,10 +546,11 @@ and solve_obligation_by_tac prg obls i tac =
true
else false
with
- | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
- | Stdpp.Exc_located(_, Refiner.FailError (_, s))
+ | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+ | Loc.Exc_located(_, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
- user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
+ user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
+ | Util.Anomaly _ as e -> raise e
| e -> false
and solve_prg_obligations prg tac =
@@ -556,7 +618,7 @@ let show_term n =
my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
@@ -568,23 +630,20 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta
else (
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;
+ progmap_add n prg;
let res = auto_solve_obligations (Some n) tactic in
match res with
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
?(hook=fun _ _ -> ()) 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) ->
- let prg = init_prog_info n (Some b) t deps (Some fixkind)
- notations obls imps kind reduce hook
- in ProgMap.add n prg acc)
- !from_prg l
- in
- from_prg := upd;
+ List.iter
+ (fun (n, b, t, imps, obls) ->
+ let prg = init_prog_info n (Some b) t deps (Some fixkind)
+ notations obls imps kind reduce hook
+ in progmap_add n prg) l;
let _defined =
List.fold_left (fun finished x ->
if finished then finished
@@ -604,8 +663,8 @@ let admit_obligations n =
match x.obl_body with
| None ->
let x = subst_deps_obl obls x in
- let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false),
- IsAssumption Conjectural)
+ let kn = Declare.declare_constant x.obl_name
+ (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
in
assumption_message x.obl_name;
obls.(i) <- { x with obl_body = Some (mkConst kn) }
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 5f6d1a2e..c1d665aa 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -8,7 +8,7 @@ open Vernacexpr
type obligation_info =
(identifier * Term.types * hole_kind located *
obligation_definition_status * Intset.t * tactic option) array
- (* ident, type, source, (opaque or transparent, expand or define),
+ (* ident, type, location, (opaque or transparent, expand or define),
dependencies, tactic to solve it *)
type progress = (* Resolution status of a program *)
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 9de7ddf2..7c0d1232 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_pretyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Global
open Pp
open Util
@@ -26,7 +24,7 @@ open List
open Recordops
open Evarutil
open Pretype_errors
-open Rawterm
+open Glob_term
open Evarconv
open Pattern
@@ -60,13 +58,10 @@ let my_print_rec_info env t =
str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
str "Full type: " ++ my_print_constr env t.f_fulltype
-(* trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *)
+(* trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *)
(* str " and tycon "++ my_print_tycon env tycon ++ *)
(* str " in environment: " ++ my_print_env env); *)
-let merge_evms x y =
- Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y
-
let interp env isevars c tycon =
let j = pretype tycon env isevars ([],[]) c in
let _ = isevars := Evarutil.nf_evar_map !isevars in
@@ -86,9 +81,9 @@ let find_with_index x l =
open Vernacexpr
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr =
+let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr =
Constrintern.intern_constr evd env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr =
+let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr =
Constrintern.intern_type evd env
let env_with_binders env isevars l =
@@ -119,14 +114,14 @@ let subtac_process ?(is_type=false) env isevars id bl c tycon =
| Some t ->
let t = Topconstr.prod_constr_expr t bl in
let t = coqintern_type !isevars env t in
- let imps = Implicit_quantifiers.implicits_of_rawterm t in
+ let imps = Implicit_quantifiers.implicits_of_glob_constr t in
let coqt, ttyp = interp env isevars t empty_tycon in
mk_tycon coqt, Some imps
in
let c = coqintern_constr !isevars env c in
let imps = match imps with
| Some i -> i
- | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c
+ | None -> Implicit_quantifiers.implicits_of_glob_constr ~with_products:is_type c
in
let coqc, ctyp = interp env isevars c tycon in
let evm = non_instanciated_map env isevars !isevars in
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 48906b23..fa767790 100644
--- a/plugins/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
@@ -13,7 +13,7 @@ module Pretyping : Pretyping.S
val interp :
Environ.env ->
Evd.evar_map ref ->
- Rawterm.rawconstr ->
+ Glob_term.glob_constr ->
Evarutil.type_constraint -> Term.constr * Term.constr
val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 4f4ae92e..d5d427c7 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -1,21 +1,18 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_pretyping_F.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
+open Compat
open Util
open Names
open Sign
open Evd
open Term
-open Termops
open Reductionops
open Environ
open Type_errors
@@ -27,7 +24,7 @@ open List
open Recordops
open Evarutil
open Pretype_errors
-open Rawterm
+open Glob_term
open Evarconv
open Pattern
open Pretyping
@@ -78,15 +75,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
for i = 0 to lt-1 do
if not (e_cumul env evdref (vdefj.(i)).uj_type
(lift lt lar.(i))) then
- error_ill_typed_rec_body_loc loc env ( !evdref)
+ error_ill_typed_rec_body_loc loc env !evdref
i lna vdefj lar
done
- let check_branches_message loc env evdref c (explft,lft) =
+ let check_branches_message loc env evdref ind c (explft,lft) =
for i = 0 to Array.length explft - 1 do
if not (e_cumul env evdref lft.(i) explft.(i)) then
let sigma = !evdref in
- error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
+ error_ill_formed_branch_loc loc env sigma c (ind,i) lft.(i) explft.(i)
done
(* coerce to tycon if any *)
@@ -99,7 +96,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(*
let evar_type_case evdref env ct pt lft p c =
let (mind,bty,rslty) = type_case_branches env ( evdref) ct pt p c
- in check_branches_message evdref env (c,ct) (bty,lft); (mind,rslty)
+ in check_branches_message evdref env mind (c,ct) (bty,lft); (mind,rslty)
*)
let strip_meta id = (* For Grammar v7 compatibility *)
@@ -108,7 +105,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
else id
let invert_ltac_bound_name env id0 id =
- try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+ try mkRel (pi1 (Termops.lookup_rel_id id (rel_context env)))
with Not_found ->
errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
str " depends on pattern variable name " ++ pr_id id ++
@@ -117,7 +114,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let pretype_id loc env sigma (lvar,unbndltacvars) id =
let id = strip_meta id in (* May happen in tactics defined by Grammar *)
try
- let (n,_,typ) = lookup_rel_id id (rel_context env) in
+ let (n,_,typ) = Termops.lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
try
@@ -153,7 +150,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let s' = mkProd (Anonymous, ind, s) in
let ccl = lift 1 (decomp n pj.uj_val) in
let ccl' = mkLambda (Anonymous, ind, ccl) in
- {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}
+ {uj_val=Termops.it_mkLambda ccl' sign; uj_type=Termops.it_mkProd s' sign}
(*************************************************************************)
(* Main pretyping function *)
@@ -162,9 +159,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let c = constr_of_global ref in
make_judge c (Retyping.get_type_of env Evd.empty c)
- let pretype_sort = function
- | RProp c -> judge_of_prop_contents c
- | RType _ -> judge_of_new_Type ()
+ let pretype_sort evdref = function
+ | GProp c -> judge_of_prop_contents c
+ | GType _ -> evd_comb0 judge_of_new_Type evdref
let split_tycon_lam loc env evd tycon =
let rec real_split evd c =
@@ -192,44 +189,44 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* in environment [env], with existential variables [( evdref)] and *)
(* the type constraint tycon *)
let rec pretype (tycon : type_constraint) env evdref lvar c =
-(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
+(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *)
(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *)
(* with _ -> () *)
(* in *)
match c with
- | RRef (loc,ref) ->
+ | GRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env evdref
(pretype_ref evdref env ref)
tycon
- | RVar (loc, id) ->
+ | GVar (loc, id) ->
inh_conv_coerce_to_tycon loc env evdref
(pretype_id loc env !evdref lvar id)
tycon
- | REvar (loc, ev, instopt) ->
+ | GEvar (loc, ev, instopt) ->
(* Ne faudrait-il pas s'assurer que hyps est bien un
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
- let hyps = evar_context (Evd.find ( !evdref) ev) in
+ let hyps = evar_context (Evd.find !evdref ev) in
let args = match instopt with
| None -> instance_from_named_context hyps
| Some inst -> failwith "Evar subtitutions not implemented" in
let c = mkEvar (ev, args) in
- let j = (Retyping.get_judgment_of env ( !evdref) c) in
+ let j = (Retyping.get_judgment_of env !evdref c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
- | RPatVar (loc,(someta,n)) ->
- anomaly "Found a pattern variable in a rawterm to type"
+ | GPatVar (loc,(someta,n)) ->
+ anomaly "Found a pattern variable in a glob_constr to type"
- | RHole (loc,k) ->
+ | GHole (loc,k) ->
let ty =
match tycon with
| Some (None, ty) -> ty
| None | Some _ ->
- e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+ e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
- | RRec (loc,fixkind,names,bl,lar,vdef) ->
+ | GRec (loc,fixkind,names,bl,lar,vdef) ->
let rec type_bl env ctxt = function
[] -> ctxt
| (na,k,None,ty)::bl ->
@@ -260,7 +257,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
push_rec_types (names,marked_ftys,[||]) env
in
- let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in
+ let fixi = match fixkind with GFix (vn, i) -> i | GCoFix i -> i in
let vdefj =
array_map2_i
(fun i ctxt def ->
@@ -284,10 +281,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
evar_type_fixpoint loc env evdref names ftys vdefj;
- let ftys = Array.map (nf_evar ( !evdref)) ftys in
- let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in
+ let ftys = Array.map (nf_evar !evdref) ftys in
+ let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
let fixj = match fixkind with
- | RFix (vn,i) ->
+ | GFix (vn,i) ->
(* First, let's find the guard indexes. *)
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
@@ -303,16 +300,17 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let fixdecls = (names,ftys,fdefs) in
let indexes = search_guard loc env possible_indexes fixdecls in
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
- | RCoFix i ->
+ | GCoFix i ->
let cofix = (i,(names,ftys,fdefs)) in
- (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+ (try check_cofix env cofix with e -> Loc.raise loc e);
make_judge (mkCoFix cofix) ftys.(i) in
inh_conv_coerce_to_tycon loc env evdref fixj tycon
- | RSort (loc,s) ->
- inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
+ | GSort (loc,s) ->
+ let s' = pretype_sort evdref s in
+ inh_conv_coerce_to_tycon loc env evdref s' tycon
- | RApp (loc,f,args) ->
+ | GApp (loc,f,args) ->
let length = List.length args in
let ftycon =
let ty =
@@ -329,13 +327,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ -> None
in
let fj = pretype ftycon env evdref lvar f in
- let floc = loc_of_rawconstr f in
+ let floc = loc_of_glob_constr f in
let rec apply_rec env n resj tycon = function
| [] -> resj
| c::rest ->
- let argloc = loc_of_rawconstr c in
+ let argloc = loc_of_glob_constr c in
let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
- let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in
+ let resty = whd_betadeltaiota env !evdref resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
Option.iter (fun ty -> evdref :=
@@ -353,10 +351,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ ->
let hj = pretype empty_tycon env evdref lvar c in
error_cant_apply_not_functional_loc
- (join_loc floc argloc) env ( !evdref)
+ (join_loc floc argloc) env !evdref
resj [hj]
in
- let resj = j_nf_evar ( !evdref) (apply_rec env 1 fj ftycon args) in
+ let resj = j_nf_evar !evdref (apply_rec env 1 fj ftycon args) in
let resj =
match kind_of_term resj.uj_val with
| App (f,args) when isInd f or isConst f ->
@@ -367,7 +365,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ -> resj in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | RLambda(loc,name,k,c1,c2) ->
+ | GLambda(loc,name,k,c1,c2) ->
let tycon' = evd_comb1
(fun evd tycon ->
match tycon with
@@ -385,32 +383,32 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let resj = judge_of_abstraction env name j j' in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | RProd(loc,name,k,c1,c2) ->
+ | GProd(loc,name,k,c1,c2) ->
let j = pretype_type empty_valcon env evdref lvar c1 in
let var = (name,j.utj_val) in
- let env' = push_rel_assum var env in
+ let env' = Termops.push_rel_assum var env in
let j' = pretype_type empty_valcon env' evdref lvar c2 in
let resj =
try judge_of_product env name j j'
- with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+ with TypeError _ as e -> Loc.raise loc e in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | RLetIn(loc,name,c1,c2) ->
+ | GLetIn(loc,name,c1,c2) ->
let j = pretype empty_tycon env evdref lvar c1 in
- let t = refresh_universes j.uj_type in
+ let t = Termops.refresh_universes j.uj_type in
let var = (name,Some j.uj_val,t) in
let tycon = lift_tycon 1 tycon in
let j' = pretype tycon (push_rel var env) evdref lvar c2 in
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
- | RLetTuple (loc,nal,(na,po),c,d) ->
+ | GLetTuple (loc,nal,(na,po),c,d) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env ( !evdref) cj.uj_type
+ try find_rectype env !evdref cj.uj_type
with Not_found ->
- let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env ( !evdref) cj
+ let cloc = loc_of_glob_constr c in
+ error_case_not_inductive_loc cloc env !evdref cj
in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 1 then
@@ -434,14 +432,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| Some p ->
let env_p = push_rels psign env in
let pj = pretype_type empty_valcon env_p evdref lvar p in
- let ccl = nf_evar ( !evdref) pj.utj_val in
+ let ccl = nf_evar !evdref pj.utj_val in
let psign = make_arity_signature env true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
let inst =
(Array.to_list cs.cs_concl_realargs)
@[build_dependent_constructor cs] in
let lp = lift cs.cs_nargs p in
- let fty = hnf_lam_applist env ( !evdref) lp inst in
+ let fty = hnf_lam_applist env !evdref lp inst in
let fj = pretype (mk_tycon fty) env_f evdref lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let v =
@@ -454,12 +452,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f evdref lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
- let ccl = nf_evar ( !evdref) fj.uj_type in
+ let ccl = nf_evar !evdref fj.uj_type in
let ccl =
if noccur_between 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl
else
- error_cant_find_case_type_loc loc env ( !evdref)
+ error_cant_find_case_type_loc loc env !evdref
cj.uj_val in
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
@@ -469,13 +467,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
{ uj_val = v; uj_type = ccl })
- | RIf (loc,c,(na,po),b1,b2) ->
+ | GIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env ( !evdref) cj.uj_type
+ try find_rectype env !evdref cj.uj_type
with Not_found ->
- let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env ( !evdref) cj in
+ let cloc = loc_of_glob_constr c in
+ error_case_not_inductive_loc cloc env !evdref cj in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 2 then
user_err_loc (loc,"",
@@ -494,7 +492,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| Some p ->
let env_p = push_rels psign env in
let pj = pretype_type empty_valcon env_p evdref lvar p in
- let ccl = nf_evar ( !evdref) pj.utj_val in
+ let ccl = nf_evar !evdref pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
@@ -505,11 +503,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let p = match tycon with
| Some (None, ty) -> ty
| None | Some _ ->
- e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
+ e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ())
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
- let pred = nf_evar ( !evdref) pred in
- let p = nf_evar ( !evdref) p in
+ let pred = nf_evar !evdref pred in
+ let p = nf_evar !evdref p in
(* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
let f cs b =
let n = rel_context_length cs.cs_args in
@@ -539,12 +537,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
{ uj_val = v; uj_type = p }
- | RCases (loc,sty,po,tml,eqns) ->
+ | GCases (loc,sty,po,tml,eqns) ->
Cases.compile_cases loc sty
((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
tycon env (* loc *) (po,tml,eqns)
- | RCast (loc,c,k) ->
+ | GCast (loc,c,k) ->
let cj =
match k with
CastCoerce ->
@@ -560,18 +558,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
inh_conv_coerce_to_tycon loc env evdref cj tycon
- | RDynamic (loc,d) ->
- if (Dyn.tag d) = "constr" then
- let c = constr_out d in
- let j = (Retyping.get_judgment_of env ( !evdref) c) in
- j
- (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
- else
- user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
-
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
and pretype_type valcon env evdref lvar = function
- | RHole loc ->
+ | GHole loc ->
(match valcon with
| Some v ->
let s =
@@ -586,12 +575,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
{ utj_val = v;
utj_type = s }
| None ->
- let s = new_Type_sort () in
+ let s = Termops.new_Type_sort () in
{ utj_val = e_new_evar evdref env ~src:loc (mkSort s);
utj_type = s})
| c ->
let j = pretype empty_tycon env evdref lvar c in
- let loc = loc_of_rawconstr c in
+ let loc = loc_of_glob_constr c in
let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
match valcon with
| None -> tj
@@ -599,7 +588,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
if e_cumul env evdref v tj.utj_val then tj
else
error_unexpected_type_loc
- (loc_of_rawconstr c) env ( !evdref) tj.utj_val v
+ (loc_of_glob_constr c) env !evdref tj.utj_val v
let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
let c' = match kind with
@@ -607,15 +596,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
(pretype tycon env evdref lvar c).uj_val
| IsType ->
- (pretype_type empty_valcon env evdref lvar c).utj_val in
- evdref := consider_remaining_unif_problems env !evdref;
- if resolve_classes then
- (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
- ~split:true ~fail:fail_evar env !evdref;
- evdref := consider_remaining_unif_problems env !evdref);
- let c = if expand_evar then nf_evar !evdref c' else c' in
- if fail_evar then check_evars env Evd.empty !evdref c;
- c
+ (pretype_type empty_valcon env evdref lvar c).utj_val
+ in
+ if resolve_classes then
+ (try
+ evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
+ ~split:true ~fail:true env !evdref;
+ evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+ ~split:true ~fail:false env !evdref
+ with e -> if fail_evar then raise e else ());
+ evdref := consider_remaining_unif_problems env !evdref;
+ let c = if expand_evar then nf_evar !evdref c' else c' in
+ if fail_evar then check_evars env Evd.empty !evdref c;
+ c
(* TODO: comment faire remonter l'information si le typage a resolu des
variables du sigma original. il faudrait que la fonction de typage
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 362c4ddc..28bbdd35 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -15,10 +15,8 @@ let ($) f x = f x
let contrib_name = "Program"
let subtac_dir = [contrib_name]
-let fix_sub_module = "Wf"
-let utils_module = "Utils"
-let fixsub_module = subtac_dir @ [fix_sub_module]
-let utils_module = subtac_dir @ [utils_module]
+let fixsub_module = subtac_dir @ ["Wf"]
+let utils_module = subtac_dir @ ["Utils"]
let tactics_module = subtac_dir @ ["Tactics"]
let init_constant dir s () = gen_constant contrib_name dir s
let init_reference dir s () = gen_reference contrib_name dir s
@@ -27,7 +25,6 @@ let safe_init_constant md name () =
check_required_library ("Coq"::md);
init_constant md name ()
-let fixsub = init_constant fixsub_module "Fix_sub"
let ex_pi1 = init_constant utils_module "ex_pi1"
let ex_pi2 = init_constant utils_module "ex_pi2"
@@ -55,11 +52,9 @@ let build_sig () =
let sig_ = build_sig
-let fix_proto = init_constant tactics_module "fix_proto"
-let fix_proto_ref () =
- match Nametab.global (make_ref "Program.Tactics.fix_proto") with
- | ConstRef c -> c
- | _ -> assert false
+let fix_proto = safe_init_constant tactics_module "fix_proto"
+
+let hide_obligation = safe_init_constant tactics_module "obligation"
let eq_ind = init_constant ["Init"; "Logic"] "eq"
let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
@@ -92,12 +87,6 @@ let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"
let proj1 = init_constant ["Init"; "Logic"] "proj1"
let proj2 = init_constant ["Init"; "Logic"] "proj2"
-let boolind = init_constant ["Init"; "Datatypes"] "bool"
-let sumboolind = init_constant ["Init"; "Specif"] "sumbool"
-let natind = init_constant ["Init"; "Datatypes"] "nat"
-let intind = init_constant ["ZArith"; "binint"] "Z"
-let existSind = init_constant ["Init"; "Specif"] "sigS"
-
let existS = build_sigma_type
let prod = build_prod
@@ -120,8 +109,8 @@ let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
let my_print_context = Termops.print_rel_context
let my_print_named_context = Termops.print_named_context
let my_print_env = Termops.print_env
-let my_print_rawconstr = Printer.pr_rawconstr_env
-let my_print_evardefs = Evd.pr_evar_map
+let my_print_glob_constr = Printer.pr_glob_constr_env
+let my_print_evardefs = Evd.pr_evar_map None
let my_print_tycon_type = Evarutil.pr_tycon_type
@@ -253,7 +242,7 @@ let build_dependent_sum l =
([intros;
(tclTHENSEQ
[constructor_tac false (Some 1) 1
- (Rawterm.ImplicitBindings [mkVar n]);
+ (Glob_term.ImplicitBindings [mkVar n]);
cont]);
])))
in
@@ -356,7 +345,7 @@ let destruct_ex ext ex =
| _ -> [acc]
in aux ex ext
-open Rawterm
+open Glob_term
let id_of_name = function
Name n -> n
@@ -418,7 +407,6 @@ let string_of_intset d =
open Printer
open Ppconstr
open Nameops
-open Termops
open Evd
let pr_meta_map evd =
@@ -430,11 +418,11 @@ let pr_meta_map evd =
| (mv,Cltyp (na,b)) ->
hov 0
(pr_meta mv ++ pr_name na ++ str " : " ++
- print_constr b.rebus ++ fnl ())
+ Termops.print_constr b.rebus ++ fnl ())
| (mv,Clval(na,b,_)) ->
hov 0
(pr_meta mv ++ pr_name na ++ str " := " ++
- print_constr (fst b).rebus ++ fnl ())
+ Termops.print_constr (fst b).rebus ++ fnl ())
in
prlist pr_meta_binding ml
@@ -445,11 +433,11 @@ let pr_evar_info evi =
(*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
Printer.pr_named_context (Global.env()) (evar_context evi)
in
- let pty = print_constr evi.evar_concl in
+ let pty = Termops.print_constr evi.evar_concl in
let pb =
match evi.evar_body with
| Evar_empty -> mt ()
- | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
+ | Evar_defined c -> spc() ++ str"=> " ++ Termops.print_constr c
in
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
@@ -463,11 +451,11 @@ let pr_evar_map sigma =
let pr_constraints pbs =
h 0
(prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
- print_constr t1 ++ spc() ++
+ Termops.print_constr t1 ++ spc() ++
str (match pbty with
| Reduction.CONV -> "=="
| Reduction.CUMUL -> "<=") ++
- spc() ++ print_constr t2) pbs)
+ spc() ++ Termops.print_constr t2) pbs)
let pr_evar_map evd =
let pp_evm =
@@ -486,4 +474,4 @@ let tactics_tac s =
lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
let tactics_call tac args =
- TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
+ TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index f56c2932..de96cc60 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -6,7 +6,7 @@ open Pp
open Evd
open Decl_kinds
open Topconstr
-open Rawterm
+open Glob_term
open Util
open Evarutil
open Names
@@ -15,11 +15,9 @@ open Sign
val ($) : ('a -> 'b) -> 'a -> 'b
val contrib_name : string
val subtac_dir : string list
-val fix_sub_module : string
val fixsub_module : string list
val init_constant : string list -> string -> constr delayed
val init_reference : string list -> string -> global_reference delayed
-val fixsub : constr delayed
val well_founded_ref : global_reference delayed
val acc_ref : global_reference delayed
val acc_inv_ref : global_reference delayed
@@ -35,7 +33,8 @@ val build_sig : unit -> coq_sigma_data
val sig_ : coq_sigma_data delayed
val fix_proto : constr delayed
-val fix_proto_ref : unit -> constant
+
+val hide_obligation : constr delayed
val eq_ind : constr delayed
val eq_rec : constr delayed
@@ -52,11 +51,6 @@ val jmeq_ind : constr delayed
val jmeq_rec : constr delayed
val jmeq_refl : constr delayed
-val boolind : constr delayed
-val sumboolind : constr delayed
-val natind : constr delayed
-val intind : constr delayed
-val existSind : constr delayed
val existS : coq_sigma_data delayed
val prod : coq_sigma_data delayed
@@ -74,7 +68,7 @@ val my_print_context : env -> std_ppcmds
val my_print_rel_context : env -> rel_context -> std_ppcmds
val my_print_named_context : env -> std_ppcmds
val my_print_env : env -> std_ppcmds
-val my_print_rawconstr : env -> rawconstr -> std_ppcmds
+val my_print_glob_constr : env -> glob_constr -> std_ppcmds
val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 22:13:06 +0000