aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml48
-rw-r--r--plugins/cc/ccalgo.mli12
-rw-r--r--plugins/cc/ccproof.ml14
-rw-r--r--plugins/cc/ccproof.mli2
-rw-r--r--plugins/cc/cctac.ml104
-rw-r--r--plugins/cc/g_congruence.ml46
6 files changed, 93 insertions, 93 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index d5d6bdf749..c01214377c 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.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 *)
@@ -25,7 +25,7 @@ let init_size=5
let cc_verbose=ref false
let debug x =
- if !cc_verbose then msg_debug x
+ if !cc_verbose then msg_debug (x ())
let _=
let gdopt=
@@ -129,14 +129,14 @@ type cinfo=
ci_nhyps: int} (* # projectable args *)
let family_eq f1 f2 = match f1, f2 with
-| InProp, InProp
-| InSet, InSet
-| InType, InType -> true
-| _ -> false
+ | Prop Pos, Prop Pos
+ | Prop Null, Prop Null
+ | Type _, Type _ -> true
+ | _ -> false
type term=
Symb of constr
- | Product of sorts_family * sorts_family
+ | Product of sorts * sorts
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -161,7 +161,7 @@ let hash_sorts_family = function
let rec hash_term = function
| Symb c -> combine 1 (hash_constr c)
- | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2)
+ | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
| Eps i -> combine 3 (Id.hash i)
| Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
| Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
@@ -425,8 +425,8 @@ let _B_ = Name (Id.of_string "A")
let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2)
let cc_product s1 s2 =
- mkLambda(_A_,mkSort(Universes.new_sort_in_family s1),
- mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_))
+ mkLambda(_A_,mkSort(s1),
+ mkLambda(_B_,mkSort(s2),_body_))
let rec constr_of_term = function
Symb s-> applist_projection s []
@@ -603,7 +603,7 @@ let add_inst state (inst,int_subst) =
Control.check_for_interrupt ();
if state.rew_depth > 0 then
if is_redundant state inst.qe_hyp_id int_subst then
- debug (str "discarding redundant (dis)equality")
+ debug (fun () -> str "discarding redundant (dis)equality")
else
begin
Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -618,7 +618,7 @@ let add_inst state (inst,int_subst) =
state.rew_depth<-pred state.rew_depth;
if inst.qe_pol then
begin
- debug (
+ debug (fun () ->
(str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
(str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " == " ++ pr_term t ++ str "]"));
@@ -626,7 +626,7 @@ let add_inst state (inst,int_subst) =
end
else
begin
- debug (
+ debug (fun () ->
(str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
(str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
@@ -657,7 +657,7 @@ let join_path uf i j=
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug (str "Linking " ++ pr_idx_term state.uf i1 ++
+ debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
str " and " ++ pr_idx_term state.uf i2 ++ str ".");
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
@@ -698,7 +698,7 @@ let union state i1 i2 eq=
let merge eq state = (* merge and no-merge *)
debug
- (str "Merging " ++ pr_idx_term state.uf eq.lhs ++
+ (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
let uf=state.uf in
let i=find uf eq.lhs
@@ -711,7 +711,7 @@ let merge eq state = (* merge and no-merge *)
let update t state = (* update 1 and 2 *)
debug
- (str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
let (i,j) as sign = signature state.uf t in
let (u,v) = subterms state.uf t in
let rep = get_representative state.uf i in
@@ -773,7 +773,7 @@ let process_constructor_mark t i rep pac state =
let process_mark t m state =
debug
- (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
let i=find state.uf t in
let rep=get_representative state.uf i in
match m with
@@ -794,7 +794,7 @@ let check_disequalities state =
else (str "No", check_aux q)
in
let _ = debug
- (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+ (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
ans
| [] -> None
@@ -824,7 +824,7 @@ let __eps__ = Id.of_string "_eps_"
let new_state_var typ state =
let id = pf_get_new_id __eps__ state.gls in
let {it=gl ; sigma=sigma} = state.gls in
- let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
+ let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in
state.gls<- gls;
id
@@ -979,7 +979,7 @@ let find_instances state =
let pb_stack= init_pb_stack state in
let res =ref [] in
let _ =
- debug (str "Running E-matching algorithm ... ");
+ debug (fun () -> str "Running E-matching algorithm ... ");
try
while true do
Control.check_for_interrupt ();
@@ -990,7 +990,7 @@ let find_instances state =
!res
let rec execute first_run state =
- debug (str "Executing ... ");
+ debug (fun () -> str "Executing ... ");
try
while
Control.check_for_interrupt ();
@@ -1000,7 +1000,7 @@ let rec execute first_run state =
None ->
if not(Int.Set.is_empty state.pa_classes) then
begin
- debug (str "First run was incomplete, completing ... ");
+ debug (fun () -> str "First run was incomplete, completing ... ");
complete state;
execute false state
end
@@ -1015,12 +1015,12 @@ let rec execute first_run state =
end
else
begin
- debug (str "Out of instances ... ");
+ debug (fun () -> str "Out of instances ... ");
None
end
else
begin
- debug (str "Out of depth ... ");
+ debug (fun () -> str "Out of depth ... ");
None
end
| Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index c72843d55f..c7fa2f56fd 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.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 *)
@@ -20,8 +20,8 @@ type pa_fun=
fnargs:int}
-module PafMap : Map.S with type key = pa_fun
-module PacMap : Map.S with type key = pa_constructor
+module PafMap : CSig.MapS with type key = pa_fun
+module PacMap : CSig.MapS with type key = pa_constructor
type cinfo =
{ci_constr: pconstructor; (* inductive type *)
@@ -30,7 +30,7 @@ type cinfo =
type term =
Symb of constr
- | Product of sorts_family * sorts_family
+ | Product of sorts * sorts
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -120,7 +120,7 @@ val term_equal : term -> term -> bool
val constr_of_term : term -> constr
-val debug : Pp.std_ppcmds -> unit
+val debug : (unit -> Pp.std_ppcmds) -> unit
val forest : state -> forest
@@ -185,7 +185,7 @@ val empty_forest: unit -> forest
(*type pa_constructor
-module PacMap:Map.S with type key=pa_constructor
+module PacMap:CSig.MapS with type key=pa_constructor
type term =
Symb of Term.constr
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 42c03234b2..d2bbaf6a7d 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.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 *)
@@ -93,13 +93,13 @@ let pinject p c n a =
p_rule=Inject(p,c,n,a)}
let rec equal_proof uf i j=
- debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
if i=j then prefl (term uf i) else
let (li,lj)=join_path uf i j in
ptrans (path_proof uf i li) (psym (path_proof uf j lj))
and edge_proof uf ((i,j),eq)=
- debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let pi=equal_proof uf i eq.lhs in
let pj=psym (equal_proof uf j eq.rhs) in
let pij=
@@ -115,7 +115,7 @@ and edge_proof uf ((i,j),eq)=
ptrans (ptrans pi pij) pj
and constr_proof uf i ipac=
- debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+ debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
let t=find_oldest_pac uf i ipac in
let eq_it=equal_proof uf i t in
if ipac.args=[] then
@@ -128,20 +128,20 @@ and constr_proof uf i ipac=
ptrans eq_it (pcongr p (prefl targ))
and path_proof uf i l=
- debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+ debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
(prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
match l with
| [] -> prefl (term uf i)
| x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
and congr_proof uf i j=
- debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let (i1,i2) = subterms uf i
and (j1,j2) = subterms uf j in
pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
and ind_proof uf i ipac j jpac=
- debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let p=equal_proof uf i j
and p1=constr_proof uf i ipac
and p2=constr_proof uf j jpac in
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 2ff2bd387a..eacbfeac70 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.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/cc/cctac.ml b/plugins/cc/cctac.ml
index 9c3a0f7299..c8924073c7 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.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 *)
@@ -22,6 +22,8 @@ open Ccproof
open Pp
open Errors
open Util
+open Proofview.Notations
+open Context.Rel.Declaration
let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
@@ -46,7 +48,7 @@ let whd_delta env=
(* decompose member of equality in an applicative format *)
(** FIXME: evar leak *)
-let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c)
+let sf_of env sigma c = e_sort_of env (ref sigma) c
let rec decompose_term env sigma t=
match kind_of_term (whd env t) with
@@ -151,7 +153,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
let patts=patterns_of_constr env sigma nrels atom in
`Nrule patts
else
- quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff
+ quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff
| _ ->
let patts=patterns_of_constr env sigma nrels term in
`Rule patts
@@ -166,7 +168,7 @@ let litteral_of_constr env sigma term=
else
begin
try
- quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff
+ quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff
with Not_found ->
`Other (decompose_term env sigma term)
end
@@ -187,7 +189,8 @@ let make_prb gls depth additionnal_terms =
let t = decompose_term env sigma c in
ignore (add_term state t)) additionnal_terms;
List.iter
- (fun (id,_,e) ->
+ (fun decl ->
+ let (id,_,e) = Context.Named.Declaration.to_tuple decl in
begin
let cid=mkVar id in
match litteral_of_constr env sigma e with
@@ -220,24 +223,9 @@ let make_prb gls depth additionnal_terms =
(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
-let build_projection intype outtype (cstr:pconstructor) special default gls=
- let env=pf_env gls in
- let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in
- let ind,u=destInd h in
- let types=Inductiveops.arities_of_constructors env (ind,u) in
- let lp=Array.length types in
- let ci=pred (snd(fst cstr)) in
- let branch i=
- let ti= prod_appvect types.(i) argv in
- let rc=fst (decompose_prod_assum ti) in
- let head=
- if Int.equal i ci then special else default in
- it_mkLambda_or_LetIn head rc in
- let branches=Array.init lp branch in
- let casee=mkRel 1 in
- let pred=mkLambda(Anonymous,intype,outtype) in
- let case_info=make_case_info (pf_env gls) ind RegularStyle in
- let body= mkCase(case_info, pred, casee, branches) in
+let build_projection intype (cstr:pconstructor) special default gls=
+ let ci= (snd(fst cstr)) in
+ let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
let id=pf_get_new_id (Id.of_string "t") gls in
mkLambda(Name id,intype,body)
@@ -254,13 +242,13 @@ let new_app_global f args k =
let new_refine c = Proofview.V82.tactic (refine c)
let assert_before n c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let evm, _ = Tacmach.New.pf_apply type_of gl c in
Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
- end
+ end }
let rec proof_tac p : unit Proofview.tactic =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
try (* type_of can raise exceptions *)
match p.p_rule with
@@ -319,16 +307,16 @@ let rec proof_tac p : unit Proofview.tactic =
let outtype = (* Termops.refresh_universes *) (type_of default) in
let special=mkRel (1+nargs-argind) in
let proj =
- Tacmach.New.of_old (build_projection intype outtype cstr special default) gl
+ Tacmach.New.of_old (build_projection intype cstr special default) gl
in
let injt=
app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
- end
+ end }
let refute_tac c t1 t2 p =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let intype =
Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
@@ -338,14 +326,14 @@ let refute_tac c t1 t2 p =
let false_t=mkApp (c,[|mkVar hid|]) in
Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
[proof_tac p; simplest_elim false_t]
- end
+ end }
let refine_exact_check c gl =
let evm, _ = pf_apply type_of gl c in
Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
let convert_to_goal_tac c t1 t2 p =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let sort =
Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
@@ -357,20 +345,20 @@ let convert_to_goal_tac c t1 t2 p =
let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
[proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
- end
+ end }
let convert_to_hyp_tac c1 t1 c2 t2 p =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let tt2=constr_of_term t2 in
let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
let false_t=mkApp (c2,[|mkVar h|]) in
Tacticals.New.tclTHENS (assert_before (Name h) tt2)
[convert_to_goal_tac c1 t1 t2 p;
simplest_elim false_t]
- end
+ end }
let discriminate_tac (cstr,u as cstru) p =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
let intype =
Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
@@ -384,11 +372,11 @@ let discriminate_tac (cstr,u as cstru) p =
let identity = Universes.constr_of_global (Lazy.force _I) in
(* let trivial=pf_unsafe_type_of gls identity in *)
let trivial = Universes.constr_of_global (Lazy.force _True) in
- let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in
+ let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in
let outtype = mkSort outtype in
let pred=mkLambda(Name xid,outtype,mkRel 1) in
let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
- let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in
+ let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
let injt=app_global _f_equal
[|intype;outtype;proj;t1;t2;mkVar hid|] in
let endt k =
@@ -399,7 +387,7 @@ let discriminate_tac (cstr,u as cstru) p =
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
(Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
[proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
- end
+ end }
(* wrap everything *)
@@ -411,18 +399,18 @@ let build_term_to_complete uf meta pac =
applistc (mkConstructU cinfo.ci_constr) all_args
let cc_tactic depth additionnal_terms =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
Coqlib.check_required_library Coqlib.logic_module_name;
- let _ = debug (Pp.str "Reading subgoal ...") in
+ let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
- let _ = debug (Pp.str "Problem built, solving ...") in
+ let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
let sol = execute true state in
- let _ = debug (Pp.str "Computation completed.") in
+ let _ = debug (fun () -> Pp.str "Computation completed.") in
let uf=forest state in
match sol with
None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
| Some reason ->
- debug (Pp.str "Goal solved, generating proof ...");
+ debug (fun () -> Pp.str "Goal solved, generating proof ...");
match reason with
Discrimination (i,ipac,j,jpac) ->
let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
@@ -462,7 +450,7 @@ let cc_tactic depth additionnal_terms =
convert_to_goal_tac id ta tb p
| HeqnH (ida,idb) ->
convert_to_hyp_tac ida ta idb tb p
- end
+ end }
let cc_fail gls =
errorlabstrm "Congruence" (Pp.str "congruence failed.")
@@ -482,19 +470,27 @@ let congruence_tac depth l =
This isn't particularly related with congruence, apart from
the fact that congruence is called internally.
*)
-
+
+let mk_eq f c1 c2 k =
+ Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let open Tacmach.New in
+ let evm, ty = pf_apply type_of gl c1 in
+ let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
+ let term = mkApp (fc, [| ty; c1; c2 |]) in
+ let evm, _ = type_of (pf_env gl) evm term in
+ Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
+ (k term)
+ end })
+
let f_equal =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let type_of = Tacmach.New.pf_unsafe_type_of gl in
let cut_eq c1 c2 =
try (* type_of can raise an exception *)
- let ty = (* Termops.refresh_universes *) (type_of c1) in
- if eq_constr_nounivs c1 c2 then Proofview.tclUNIT ()
- else
- Tacticals.New.tclTRY (Tacticals.New.tclTHEN
- ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
- (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
+ Tacticals.New.tclTHENS
+ (mk_eq _eq c1 c2 Tactics.cut)
+ [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)]
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
Proofview.tclORELSE
@@ -514,4 +510,4 @@ let f_equal =
| Type_errors.TypeError _ -> Proofview.tclUNIT ()
| e -> Proofview.tclZERO ~info e
end
- end
+ end }
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index aa31c6f078..9a53e2e16a 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.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 *)
@@ -9,6 +9,10 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Cctac
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
DECLARE PLUGIN "cc_plugin"
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 21:56:34 +0000