aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml24
-rw-r--r--plugins/firstorder/formula.mli8
-rw-r--r--plugins/firstorder/g_ground.ml441
-rw-r--r--plugins/firstorder/ground.ml8
-rw-r--r--plugins/firstorder/ground.mli2
-rw-r--r--plugins/firstorder/ground_plugin.mlpack (renamed from plugins/firstorder/ground_plugin.mllib)1
-rw-r--r--plugins/firstorder/instances.ml53
-rw-r--r--plugins/firstorder/instances.mli2
-rw-r--r--plugins/firstorder/rules.ml29
-rw-r--r--plugins/firstorder/rules.mli2
-rw-r--r--plugins/firstorder/sequent.ml11
-rw-r--r--plugins/firstorder/sequent.mli4
-rw-r--r--plugins/firstorder/unify.ml2
-rw-r--r--plugins/firstorder/unify.mli2
14 files changed, 102 insertions, 87 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 62a8605a3d..b34a364920 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -16,9 +16,11 @@ open Util
open Declarations
open Globnames
+module RelDecl = Context.Rel.Declaration
+
let qflag=ref true
-let red_flags=ref Closure.betaiotazeta
+let red_flags=ref CClosure.betaiotazeta
let (=?) f g i1 i2 j1 j2=
let c=f i1 i2 in
@@ -58,12 +60,12 @@ let ind_hyps nevar ind largs gls=
Array.map myhyps types
let special_nf gl=
- let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
- (fun t -> Closure.norm_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+ (fun t -> CClosure.norm_val infos (CClosure.inject t))
let special_whd gl=
- let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
- (fun t -> Closure.whd_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+ (fun t -> CClosure.whd_val infos (CClosure.inject t))
type kind_of_formula=
Arrow of constr*constr
@@ -139,8 +141,8 @@ let build_atoms gl metagen side cciterm =
negative:= unsigned :: !negative
end;
let v = ind_hyps 0 i l gl in
- let g i _ (_,_,t) =
- build_rec env polarity (lift i t) in
+ let g i _ decl =
+ build_rec env polarity (lift i (RelDecl.get_type decl)) in
let f l =
List.fold_left_i g (1-(List.length l)) () l in
if polarity && (* we have a constant constructor *)
@@ -150,8 +152,8 @@ let build_atoms gl metagen side cciterm =
| Exists(i,l)->
let var=mkMeta (metagen true) in
let v =(ind_hyps 1 i l gl).(0) in
- let g i _ (_,_,t) =
- build_rec (var::env) polarity (lift i t) in
+ let g i _ decl =
+ build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in
List.fold_left_i g (2-(List.length l)) () v
| Forall(_,b)->
let var=mkMeta (metagen true) in
@@ -224,7 +226,7 @@ let build_formula side nam typ gl metagen=
| And(_,_,_) -> Rand
| Or(_,_,_) -> Ror
| Exists (i,l) ->
- let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
+ let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in
Rexists(m,d,trivial)
| Forall (_,a) -> Rforall
| Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 29ea1e7770..5db8ff59ad 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -1,19 +1,17 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Term
-open Context
open Globnames
val qflag : bool ref
-val red_flags: Closure.RedFlags.reds ref
+val red_flags: CClosure.RedFlags.reds ref
val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
'a -> 'a -> 'b -> 'b -> int
@@ -28,7 +26,7 @@ type counter = bool -> metavariable
val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
val ind_hyps : int -> pinductive -> constr list ->
- Proof_type.goal Tacmach.sigma -> rel_context array
+ Proof_type.goal Tacmach.sigma -> Context.Rel.t array
type atoms = {positive:constr list;negative:constr list}
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c28da42aea..260e86ad67 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -15,6 +15,9 @@ open Goptions
open Tacticals
open Tacinterp
open Libnames
+open Stdarg
+open Tacarg
+open Pcoq.Prim
DECLARE PLUGIN "ground_plugin"
@@ -52,8 +55,15 @@ let _=
in
declare_int_option gdopt
+let default_intuition_tac =
+ let tac _ _ = Auto.h_auto None [] None in
+ let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
+ let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
+ Tacenv.register_ml_tactic name [| tac |];
+ Tacexpr.TacML (Loc.ghost, entry, [])
+
let (set_default_solver, default_solver, print_default_solver) =
- Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver"
+ Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
@@ -64,7 +74,7 @@ END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> [
- Pp.msg_info
+ Feedback.msg_info
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
END
@@ -106,11 +116,17 @@ open Pp
open Genarg
open Ppconstr
open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
+
+let warn_deprecated_syntax =
+ CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
+ (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
+
ARGUMENT EXTEND firstorder_using
+ TYPED AS reference_list
PRINTED BY pr_firstorder_using_typed
RAW_TYPED AS reference_list
RAW_PRINTED BY pr_firstorder_using_raw
@@ -119,8 +135,7 @@ ARGUMENT EXTEND firstorder_using
| [ "using" reference(a) ] -> [ [a] ]
| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
| [ "using" reference(a) reference(b) reference_list(l) ] -> [
- Flags.if_verbose
- Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+ warn_deprecated_syntax ();
a::b::l
]
| [ ] -> [ [] ]
@@ -128,20 +143,22 @@ END
TACTIC EXTEND firstorder
[ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ]
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ]
END
TACTIC EXTEND gintuition
[ "gintuition" tactic_opt(t) ] ->
- [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ]
+ [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ]
END
open Proofview.Notations
+open Cc_plugin
+open Decl_mode_plugin
let default_declarative_automation =
Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 2248b66931..628af4e719 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,15 +24,15 @@ let update_flags ()=
in
List.iter f (Classops.coercions ());
red_flags:=
- Closure.RedFlags.red_add_transparent
- Closure.betaiotazeta
+ CClosure.RedFlags.red_add_transparent
+ CClosure.betaiotazeta
(Names.Id.Pred.full,Names.Cpred.complement !predref)
let ground_tac solver startseq gl=
update_flags ();
let rec toptac skipped seq gl=
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
- then Pp.msg_debug (Printer.pr_goal gl);
+ then Feedback.msg_debug (Printer.pr_goal gl);
tclORELSE (axiom_tac seq.gl seq)
begin
try
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 5b32078601..b5669463cd 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mlpack
index 447a1fb513..65fb2e9a1d 100644
--- a/plugins/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mlpack
@@ -5,4 +5,3 @@ Rules
Instances
Ground
G_ground
-Ground_plugin_mod
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a88778c739..eebd974ea8 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,11 +8,10 @@
open Unify
open Rules
-open Errors
+open CErrors
open Util
open Term
open Vars
-open Glob_term
open Tacmach
open Tactics
open Tacticals
@@ -22,6 +21,8 @@ open Formula
open Sequent
open Names
open Misctypes
+open Sigma.Notations
+open Context.Rel.Declaration
let compare_instance inst1 inst2=
match inst1,inst2 with
@@ -96,8 +97,6 @@ let rec collect_quantified seq=
(* open instances processor *)
-let dummy_constr=mkMeta (-1)
-
let dummy_bvid=Id.of_string "x"
let mk_open_instance id idc gl m t=
@@ -105,32 +104,24 @@ let mk_open_instance id idc gl m t=
let evmap=Refiner.project gl in
let var_id=
if id==dummy_id then dummy_bvid else
- let typ=pf_type_of gl idc in
+ let typ=pf_unsafe_type_of gl idc in
(* since we know we will get a product,
reduction is not too expensive *)
- let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
+ let (nam,_,_)=destProd (whd_all env evmap typ) in
match nam with
Name id -> id
| Anonymous -> dummy_bvid in
let revt=substl (List.init m (fun i->mkRel (m-i))) t in
- let rec aux n avoid=
- if Int.equal n 0 then [] else
+ let rec aux n avoid env evmap decls =
+ if Int.equal n 0 then evmap, decls else
let nid=(fresh_id avoid var_id gl) in
- (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
- let nt=it_mkLambda_or_LetIn revt (aux m []) in
- let rawt=Detyping.detype false [] env evmap nt in
- let rec raux n t=
- if Int.equal n 0 then t else
- match t with
- GLambda(loc,name,k,_,t0)->
- let t1=raux (n-1) t0 in
- GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1)
- | _-> anomaly (Pp.str "can't happen") in
- let ntt=try
- fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)
- with e when Errors.noncritical e ->
- error "Untypable instance, maybe higher-order non-prenex quantification" in
- decompose_lam_n_assum m ntt
+ let evmap = Sigma.Unsafe.of_evar_map evmap in
+ let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+ let evmap = Sigma.to_evar_map evmap in
+ let decl = LocalAssum (Name nid, c) in
+ aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+ let evmap, decls = aux m [] env evmap [] in
+ evmap, decls, revt
(* tactics *)
@@ -144,9 +135,9 @@ let left_instance_tac (inst,id) continue seq=
[tclTHENLIST
[Proofview.V82.of_tactic introf;
pf_constr_of_global id (fun idc ->
- (fun gls->generalize
+ (fun gls-> Proofview.V82.of_tactic (generalize
[mkApp(idc,
- [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
+ [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
Proofview.V82.of_tactic introf;
tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
@@ -159,14 +150,18 @@ let left_instance_tac (inst,id) continue seq=
if m>0 then
pf_constr_of_global id (fun idc ->
fun gl->
- let (rc,ot) = mk_open_instance id idc gl m t in
+ let evmap,rc,ot = mk_open_instance id idc gl m t in
let gt=
it_mkLambda_or_LetIn
(mkApp(idc,[|ot|])) rc in
- generalize [gt] gl)
+ let evmap, _ =
+ try Typing.type_of (pf_env gl) evmap gt
+ with e when CErrors.noncritical e ->
+ error "Untypable instance, maybe higher-order non-prenex quantification" in
+ tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
else
pf_constr_of_global id (fun idc ->
- generalize [mkApp(idc,[|t|])])
+ Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
in
tclTHENLIST
[special_generalize;
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 2f69ad7b51..ce711f3f97 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 382d5409b1..7ffc78928d 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -20,6 +20,8 @@ open Sequent
open Globnames
open Locus
+module NamedDecl = Context.Named.Declaration
+
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
type lseqtac= global_reference -> seqtac
@@ -34,12 +36,13 @@ let wrap n b continue seq gls=
if i<=0 then seq else
match nc with
[]->anomaly (Pp.str "Not the expected number of hyps")
- | ((id,_,typ) as nd)::q->
+ | nd::q->
+ let id = NamedDecl.get_id nd in
if occur_var env id (pf_concl gls) ||
List.exists (occur_var_in_decl env id) ctx then
(aux (i-1) q (nd::ctx))
else
- add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
+ add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
let seq1=aux n nc [] in
let seq2=if b then
add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
@@ -50,13 +53,13 @@ let basename_of_global=function
| _->assert false
let clear_global=function
- VarRef id->clear [id]
+ VarRef id-> Proofview.V82.of_tactic (clear [id])
| _->tclIDTAC
(* connection rules *)
let axiom_tac t seq=
- try pf_constr_of_global (find_left t seq) exact_no_check
+ try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
@@ -65,7 +68,7 @@ let ll_atom_tac a backtrack id continue seq=
tclTHENLIST
[pf_constr_of_global (find_left a seq) (fun left ->
pf_constr_of_global id (fun id ->
- generalize [mkApp(id, [|left|])]));
+ Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
clear_global id;
Proofview.V82.of_tactic intro]
with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -133,7 +136,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
let newhyps idc =List.init lp (myterm idc) in
tclIFTHENELSE
(tclTHENLIST
- [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
+ [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
clear_global id;
tclDO lp (Proofview.V82.of_tactic intro)])
(wrap lp false continue seq) backtrack gl
@@ -149,9 +152,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
clear_global id;
wrap 1 false continue seq];
tclTHENS (Proofview.V82.of_tactic (cut cc))
- [pf_constr_of_global id exact_no_check;
+ [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
tclTHENLIST
- [pf_constr_of_global id (fun idc -> generalize [d idc]);
+ [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
clear_global id;
Proofview.V82.of_tactic introf;
Proofview.V82.of_tactic introf;
@@ -190,7 +193,7 @@ let ll_forall_tac prod backtrack id continue seq=
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
let term=mkApp(idc,[|mkVar(id0)|]) in
- tclTHEN (generalize [term]) (clear [id0]) gls));
+ tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
clear_global id;
Proofview.V82.of_tactic intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
@@ -210,6 +213,6 @@ let defined_connectives=lazy
let normalize_evaluables=
onAllHypsAndConcl
(function
- None->unfold_in_concl (Lazy.force defined_connectives)
+ None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
| Some id ->
- unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+ Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 596e8535f6..381b7cd87c 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2f7f21e418..1248b60a76 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -1,13 +1,13 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Term
-open Errors
+open CErrors
open Util
open Formula
open Unify
@@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl =
let l = expand_constructor_hints l in
let f gr (seq,gl) =
let gl, c = pf_eapply Evd.fresh_global gl gr in
- let typ=(pf_type_of gl c) in
+ let typ=(pf_unsafe_type_of gl c) in
(add_formula Hyp gr typ seq gl,gl) in
List.fold_right f l (seq,gl)
@@ -209,12 +209,13 @@ open Hints
let extend_with_auto_hints l seq gl=
let seqref=ref seq in
let f p_a_t =
- match p_a_t.code with
+ match repr_hint p_a_t.code with
Res_pf (c,_) | Give_exact (c,_)
| Res_pf_THEN_trivial_fail (c,_) ->
+ let (c, _, _) = c in
(try
let gr = global_of_constr c in
- let typ=(pf_type_of gl c) in
+ let typ=(pf_unsafe_type_of gl c) in
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
| _-> () in
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index dc3f05be69..06c9251e7b 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -13,7 +13,7 @@ open Globnames
module OrderedConstr: Set.OrderedType with type t=constr
-module CM: Map.S with type key=constr
+module CM: CSig.MapS with type key=constr
type h_item = global_reference * (int*constr) option
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 0a17203408..d9ab36ad64 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 1531854679..4fe9ad38d8 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:11:08 +0000