summaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml122
-rw-r--r--plugins/cc/ccalgo.mli22
-rw-r--r--plugins/cc/ccproof.ml16
-rw-r--r--plugins/cc/ccproof.mli12
-rw-r--r--plugins/cc/cctac.ml337
-rw-r--r--plugins/cc/cctac.mli16
-rw-r--r--plugins/cc/g_congruence.ml414
7 files changed, 278 insertions, 261 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113..8e53a044 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,24 +1,26 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This file implements the basic congruence-closure algorithm by *)
-(* Downey,Sethi and Tarjan. *)
+(* Downey, Sethi and Tarjan. *)
(* Plus some e-matching and constructor handling by P. Corbineau *)
open CErrors
-open Util
open Pp
-open Goptions
open Names
-open Term
+open Sorts
+open Constr
open Vars
+open Goptions
open Tacmach
-open Evd
+open Util
let init_size=5
@@ -29,8 +31,7 @@ let debug x =
let _=
let gdopt=
- { optsync=true;
- optdepr=false;
+ { optdepr=false;
optname="Congruence Verbose";
optkey=["Congruence";"Verbose"];
optread=(fun ()-> !cc_verbose);
@@ -62,7 +63,7 @@ module ST=struct
let enter t sign st=
if IntPairTable.mem st.toterm sign then
- anomaly ~label:"enter" (Pp.str "signature already entered")
+ anomaly ~label:"enter" (Pp.str "signature already entered.")
else
IntPairTable.replace st.toterm sign t;
IntTable.replace st.tosign t sign
@@ -136,7 +137,7 @@ let family_eq f1 f2 = match f1, f2 with
type term=
Symb of constr
- | Product of sorts * sorts
+ | Product of Sorts.t * Sorts.t
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -155,7 +156,7 @@ let rec term_equal t1 t2 =
open Hashset.Combine
let rec hash_term = function
- | Symb c -> combine 1 (hash_constr c)
+ | Symb c -> combine 1 (Constr.hash c)
| 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)
@@ -216,7 +217,7 @@ type representative=
mutable lfathers:Int.Set.t;
mutable fathers:Int.Set.t;
mutable inductive_status: inductive_status;
- class_type : Term.types;
+ class_type : types;
mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
type cl = Rep of representative| Eqto of int*equality
@@ -233,7 +234,7 @@ type node =
module Constrhash = Hashtbl.Make
(struct type t = constr
let equal = eq_constr_nounivs
- let hash = hash_constr
+ let hash = Constr.hash
end)
module Typehash = Constrhash
@@ -270,7 +271,8 @@ type state =
mutable rew_depth:int;
mutable changed:bool;
by_type: Int.Set.t Typehash.t;
- mutable gls:Proof_type.goal Tacmach.sigma}
+ mutable env:Environ.env;
+ sigma:Evd.evar_map}
let dummy_node =
{
@@ -305,7 +307,8 @@ let empty depth gls:state =
rew_depth=depth;
by_type=Constrhash.create init_size;
changed=false;
- gls=gls
+ env=pf_env gls;
+ sigma=project gls
}
let forest state = state.uf
@@ -322,7 +325,7 @@ let find uf i= find_aux uf [] i
let get_representative uf i=
match uf.map.(i).clas with
Rep r -> r
- | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative")
+ | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative.")
let get_constructors uf i= uf.map.(i).constructors
@@ -340,7 +343,7 @@ let rec find_oldest_pac uf i pac=
let get_constructor_info uf i=
match uf.map.(i).term with
Constructor cinfo->cinfo
- | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor")
+ | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor.")
let size uf i=
(get_representative uf i).weight
@@ -385,7 +388,7 @@ let term uf i=uf.map.(i).term
let subterms uf i=
match uf.map.(i).vertex with
Node(j,k) -> (j,k)
- | _ -> anomaly ~label:"subterms" (Pp.str "not a node")
+ | _ -> anomaly ~label:"subterms" (Pp.str "not a node.")
let signature uf i=
let j,k=subterms uf i in (find uf j,find uf k)
@@ -424,7 +427,7 @@ let cc_product s1 s2 =
mkLambda(_B_,mkSort(s2),_body_))
let rec constr_of_term = function
- Symb s-> applist_projection s []
+ Symb s-> s
| Product(s1,s2) -> cc_product s1 s2
| Eps id -> mkVar id
| Constructor cinfo -> mkConstructU cinfo.ci_constr
@@ -432,37 +435,20 @@ let rec constr_of_term = function
make_app [(constr_of_term s2)] s1
and make_app l=function
Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
- | other ->
- applist_proj other l
-and applist_proj c l =
- match c with
- | Symb s -> applist_projection s l
- | _ -> applistc (constr_of_term c) l
-and applist_projection c l =
- match kind_of_term c with
- | Const c when Environ.is_projection (fst c) (Global.env()) ->
- let p = Projection.make (fst c) false in
- (match l with
- | [] -> (* Expand the projection *)
- let ty,_ = Typeops.type_of_constant (Global.env ()) c in
- let pb = Environ.lookup_projection p (Global.env()) in
- let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
- it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
- | hd :: tl ->
- applistc (mkProj (p, hd)) tl)
- | _ -> applistc c l
-
-let rec canonize_name c =
- let func = canonize_name in
- match kind_of_term c with
+ | other -> Term.applist (constr_of_term other,l)
+
+let rec canonize_name sigma c =
+ let c = EConstr.Unsafe.to_constr c in
+ let func c = canonize_name sigma (EConstr.of_constr c) in
+ match Constr.kind c with
| Const (kn,u) ->
- let canon_const = constant_of_kn (canonical_con kn) in
+ let canon_const = Constant.make1 (Constant.canonical kn) in
(mkConstU (canon_const,u))
| Ind ((kn,i),u) ->
- let canon_mind = mind_of_kn (canonical_mind kn) in
+ let canon_mind = MutInd.make1 (MutInd.canonical kn) in
(mkIndU ((canon_mind,i),u))
| Construct (((kn,i),j),u) ->
- let canon_mind = mind_of_kn (canonical_mind kn) in
+ let canon_mind = MutInd.make1 (MutInd.canonical kn) in
mkConstructU (((canon_mind,i),j),u)
| Prod (na,t,ct) ->
mkProd (na,func t, func ct)
@@ -474,7 +460,7 @@ let rec canonize_name c =
mkApp (func ct,Array.smartmap func l)
| Proj(p,c) ->
let p' = Projection.map (fun kn ->
- constant_of_kn (canonical_con kn)) p in
+ Constant.make1 (Constant.canonical kn)) p in
(mkProj (p', func c))
| _ -> c
@@ -485,7 +471,7 @@ let build_subst uf subst =
(fun i ->
try term uf i
with e when CErrors.noncritical e ->
- anomaly (Pp.str "incomplete matching"))
+ anomaly (Pp.str "incomplete matching."))
subst
let rec inst_pattern subst = function
@@ -497,10 +483,10 @@ let rec inst_pattern subst = function
args t
let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
- Termops.print_constr (constr_of_term (term uf i)) ++ str "]"
+ Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
let pr_term t = str "[" ++
- Termops.print_constr (constr_of_term t) ++ str "]"
+ Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
let rec add_term state t=
let uf=state.uf in
@@ -508,8 +494,8 @@ let rec add_term state t=
Not_found ->
let b=next uf in
let trm = constr_of_term t in
- let typ = pf_unsafe_type_of state.gls trm in
- let typ = canonize_name typ in
+ let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in
+ let typ = canonize_name state.sigma typ in
let new_node=
match t with
Symb _ | Product (_,_) ->
@@ -615,7 +601,7 @@ let add_inst state (inst,int_subst) =
begin
debug (fun () ->
(str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
- (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
pr_term s ++ str " == " ++ pr_term t ++ str "]"));
add_equality state prf s t
end
@@ -623,7 +609,7 @@ let add_inst state (inst,int_subst) =
begin
debug (fun () ->
(str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
- (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
add_disequality state (Hyp prf) s t
end
@@ -750,7 +736,7 @@ let process_constructor_mark t i rep pac state =
state.combine;
f (n-1) q1 q2
| _-> anomaly ~label:"add_pacs"
- (Pp.str "weird error in injection subterms merge")
+ (Pp.str "weird error in injection subterms merge.")
in f cinfo.ci_nhyps opac.args pac.args
| Partial_applied | Partial _ ->
(* add_pac state.uf.map.(i) pac t; *)
@@ -817,11 +803,10 @@ let one_step state =
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 [Context.Named.Declaration.LocalAssum (id,typ)] in
- state.gls<- gls;
- id
+ let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in
+ let id = Namegen.next_ident_away __eps__ ids in
+ state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env;
+ id
let complete_one_class state i=
match (get_representative state.uf i).inductive_status with
@@ -829,18 +814,19 @@ let complete_one_class state i=
let rec app t typ n =
if n<=0 then t else
let _,etyp,rest= destProd typ in
- let id = new_state_var etyp state in
+ let id = new_state_var (EConstr.of_constr etyp) state in
app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
- let _c = pf_unsafe_type_of state.gls
- (constr_of_term (term state.uf pac.cnode)) in
+ let _c = Typing.unsafe_type_of state.env state.sigma
+ (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+ let _c = EConstr.Unsafe.to_constr _c in
let _args =
List.map (fun i -> constr_of_term (term state.uf i))
pac.args in
- let typ = prod_applist _c (List.rev _args) in
+ let typ = Term.prod_applist _c (List.rev _args) in
let ct = app (term state.uf i) typ pac.arity in
state.uf.epsilons <- pac :: state.uf.epsilons;
ignore (add_term state ct)
- | _ -> anomaly (Pp.str "wrong incomplete class")
+ | _ -> anomaly (Pp.str "wrong incomplete class.")
let complete state =
Int.Set.iter (complete_one_class state) state.pa_classes
@@ -980,7 +966,7 @@ let find_instances state =
Control.check_for_interrupt ();
do_match state res pb_stack
done;
- anomaly (Pp.str "get out of here !")
+ anomaly (Pp.str "get out of here!")
with Stack.Empty -> () in
!res
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index c7fa2f56..4ebc6a13 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,13 +1,15 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
-open Term
+open Constr
open Names
type pa_constructor =
@@ -30,7 +32,7 @@ type cinfo =
type term =
Symb of constr
- | Product of sorts * sorts
+ | Product of Sorts.t * Sorts.t
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -85,7 +87,7 @@ type representative=
mutable lfathers:Int.Set.t;
mutable fathers:Int.Set.t;
mutable inductive_status: inductive_status;
- class_type : Term.types;
+ class_type : types;
mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
type cl = Rep of representative| Eqto of int*equality
@@ -120,7 +122,7 @@ val term_equal : term -> term -> bool
val constr_of_term : term -> constr
-val debug : (unit -> Pp.std_ppcmds) -> unit
+val debug : (unit -> Pp.t) -> unit
val forest : state -> forest
@@ -128,7 +130,7 @@ val axioms : forest -> (term * term) Constrhash.t
val epsilons : forest -> pa_constructor list
-val empty : int -> Proof_type.goal Tacmach.sigma -> state
+val empty : int -> Goal.goal Evd.sigma -> state
val add_term : state -> term -> int
@@ -169,7 +171,7 @@ val find_instances : state -> (quant_eq * int array) list
val execute : bool -> state -> explanation option
-val pr_idx_term : forest -> int -> Pp.std_ppcmds
+val pr_idx_term : forest -> int -> Pp.t
val empty_forest: unit -> forest
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index f58847ca..1f1fa9c9 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -1,16 +1,18 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
open CErrors
-open Term
+open Constr
open Ccalgo
open Pp
@@ -47,7 +49,7 @@ let rec ptrans p1 p3=
{p_lhs=p1.p_lhs;
p_rhs=p3.p_rhs;
p_rule=Trans (p1,p3)}
- else anomaly (Pp.str "invalid cc transitivity")
+ else anomaly (Pp.str "invalid cc transitivity.")
let rec psym p =
match p.p_rule with
@@ -85,7 +87,7 @@ let rec nth_arg t n=
if n>0 then
nth_arg t1 (n-1)
else t2
- | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args")
+ | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args.")
let pinject p c n a =
{p_lhs=nth_arg p.p_lhs (n-a);
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index eacbfeac..bebef241 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -1,13 +1,15 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Ccalgo
-open Term
+open Constr
type rule=
Ax of constr
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index fd46d806..d19817e7 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This file is the interface between the c-c algorithm and Coq *)
@@ -12,20 +14,21 @@ open Evd
open Names
open Inductiveops
open Declarations
-open Term
+open Constr
+open EConstr
open Vars
-open Tacmach
open Tactics
open Typing
open Ccalgo
open Ccproof
open Pp
-open CErrors
open Util
open Proofview.Notations
-open Context.Rel.Declaration
-let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
+let reference dir s = lazy (Coqlib.coq_reference "CC" dir s)
let _f_equal = reference ["Init";"Logic"] "f_equal"
let _eq_rect = reference ["Init";"Logic"] "eq_rect"
@@ -37,13 +40,11 @@ let _False = reference ["Init";"Logic"] "False"
let _True = reference ["Init";"Logic"] "True"
let _I = reference ["Init";"Logic"] "I"
-let whd env=
- let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in
- (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let whd env sigma t =
+ Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t
-let whd_delta env=
- let infos=CClosure.create_clos_infos CClosure.all env in
- (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let whd_delta env sigma t =
+ Reductionops.clos_whd_flags CClosure.all env sigma t
(* decompose member of equality in an applicative format *)
@@ -51,12 +52,12 @@ let whd_delta env=
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
+ match EConstr.kind sigma (whd env sigma t) with
App (f,args)->
let tf=decompose_term env sigma f in
let targs=Array.map (decompose_term env sigma) args in
Array.fold_left (fun s t->Appli (s,t)) tf targs
- | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+ | Prod (_,a,_b) when noccurn sigma 1 _b ->
let b = Termops.pop _b in
let sort_b = sf_of env sigma b in
let sort_a = sf_of env sigma a in
@@ -65,7 +66,8 @@ let rec decompose_term env sigma t=
decompose_term env sigma b)
| Construct c ->
let (((mind,i_ind),i_con),u)= c in
- let canon_mind = mind_of_kn (canonical_mind mind) in
+ let u = EInstance.kind sigma u in
+ let canon_mind = MutInd.make1 (MutInd.canonical mind) in
let canon_ind = canon_mind,i_ind in
let (oib,_)=Global.lookup_inductive (canon_ind) in
let nargs=constructor_nallargs_env env (canon_ind,i_con) in
@@ -74,28 +76,31 @@ let rec decompose_term env sigma t=
ci_nhyps=nargs-oib.mind_nparams}
| Ind c ->
let (mind,i_ind),u = c in
- let canon_mind = mind_of_kn (canonical_mind mind) in
- let canon_ind = canon_mind,i_ind in (Symb (mkIndU (canon_ind,u)))
+ let u = EInstance.kind sigma u in
+ let canon_mind = MutInd.make1 (MutInd.canonical mind) in
+ let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u)))
| Const (c,u) ->
- let canon_const = constant_of_kn (canonical_con c) in
- (Symb (mkConstU (canon_const,u)))
+ let u = EInstance.kind sigma u in
+ let canon_const = Constant.make1 (Constant.canonical c) in
+ (Symb (Constr.mkConstU (canon_const,u)))
| Proj (p, c) ->
- let canon_const kn = constant_of_kn (canonical_con kn) in
+ let canon_const kn = Constant.make1 (Constant.canonical kn) in
let p' = Projection.map canon_const p in
- (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
+ let c = Retyping.expand_projection env sigma p' c [] in
+ decompose_term env sigma c
| _ ->
- let t = strip_outer_cast t in
- if closed0 t then Symb t else raise Not_found
+ let t = Termops.strip_outer_cast sigma t in
+ if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
(* decompose equality in members and type *)
-open Globnames
+open Termops
let atom_of_constr env sigma term =
- let wh = (whd_delta env term) in
- let kot = kind_of_term wh in
+ let wh = whd_delta env sigma term in
+ let kot = EConstr.kind sigma wh in
match kot with
App (f,args)->
- if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
+ if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
then `Eq (args.(0),
decompose_term env sigma args.(1),
decompose_term env sigma args.(2))
@@ -103,14 +108,14 @@ let atom_of_constr env sigma term =
| _ -> `Other (decompose_term env sigma term)
let rec pattern_of_constr env sigma c =
- match kind_of_term (whd env c) with
+ match EConstr.kind sigma (whd env sigma c) with
App (f,args)->
let pf = decompose_term env sigma f in
let pargs,lrels = List.split
(Array.map_to_list (pattern_of_constr env sigma) args) in
PApp (pf,List.rev pargs),
List.fold_left Int.Set.union Int.Set.empty lrels
- | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+ | Prod (_,a,_b) when noccurn sigma 1 _b ->
let b = Termops.pop _b in
let pa,sa = pattern_of_constr env sigma a in
let pb,sb = pattern_of_constr env sigma b in
@@ -129,19 +134,19 @@ let non_trivial = function
let patterns_of_constr env sigma nrels term=
let f,args=
- try destApp (whd_delta env term) with DestKO -> raise Not_found in
- if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
+ try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in
+ if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
then
let patt1,rels1 = pattern_of_constr env sigma args.(1)
and patt2,rels2 = pattern_of_constr env sigma args.(2) in
let valid1 =
if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
else if non_trivial patt1 then Normal
- else Trivial args.(0)
+ else Trivial (EConstr.to_constr sigma args.(0))
and valid2 =
if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
else if non_trivial patt2 then Normal
- else Trivial args.(0) in
+ else Trivial (EConstr.to_constr sigma args.(0)) in
if valid1 != Creates_variables
|| valid2 != Creates_variables then
nrels,valid1,patt1,valid2,patt2
@@ -149,28 +154,28 @@ let patterns_of_constr env sigma nrels term=
else raise Not_found
let rec quantified_atom_of_constr env sigma nrels term =
- match kind_of_term (whd_delta env term) with
+ match EConstr.kind sigma (whd_delta env sigma term) with
Prod (id,atom,ff) ->
- if is_global (Lazy.force _False) ff then
+ if is_global sigma (Lazy.force _False) ff then
let patts=patterns_of_constr env sigma nrels atom in
`Nrule patts
else
- quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff
+ quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
| _ ->
let patts=patterns_of_constr env sigma nrels term in
`Rule patts
let litteral_of_constr env sigma term=
- match kind_of_term (whd_delta env term) with
+ match EConstr.kind sigma (whd_delta env sigma term) with
| Prod (id,atom,ff) ->
- if is_global (Lazy.force _False) ff then
+ if is_global sigma (Lazy.force _False) ff then
match (atom_of_constr env sigma atom) with
`Eq(t,a,b) -> `Neq(t,a,b)
| `Other(p) -> `Nother(p)
else
begin
try
- quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff
+ quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
with Not_found ->
`Other (decompose_term env sigma term)
end
@@ -181,9 +186,10 @@ let litteral_of_constr env sigma term=
(* store all equalities from the context *)
let make_prb gls depth additionnal_terms =
+ let open Tacmach.New in
let env=pf_env gls in
- let sigma=sig_sig gls in
- let state = empty depth gls in
+ let sigma=project gls in
+ let state = empty depth {it = Proofview.Goal.goal gls; sigma } in
let pos_hyps = ref [] in
let neg_hyps =ref [] in
List.iter
@@ -192,10 +198,10 @@ let make_prb gls depth additionnal_terms =
ignore (add_term state t)) additionnal_terms;
List.iter
(fun decl ->
- let (id,_,e) = Context.Named.Declaration.to_tuple decl in
+ let id = NamedDecl.get_id decl in
begin
- let cid=mkVar id in
- match litteral_of_constr env sigma e with
+ let cid=Constr.mkVar id in
+ match litteral_of_constr env sigma (NamedDecl.get_type decl) with
`Eq (t,a,b) -> add_equality state cid a b
| `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
| `Other ph ->
@@ -212,9 +218,9 @@ let make_prb gls depth additionnal_terms =
neg_hyps:=(cid,nh):: !neg_hyps
| `Rule patts -> add_quant state id true patts
| `Nrule patts -> add_quant state id false patts
- end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
+ end) (Proofview.Goal.hyps gls);
begin
- match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with
+ match atom_of_constr env sigma (pf_concl gls) with
`Eq (t,a,b) -> add_disequality state Goal a b
| `Other g ->
List.iter
@@ -226,63 +232,88 @@ let make_prb gls depth additionnal_terms =
(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
let build_projection intype (cstr:pconstructor) special default gls=
+ let open Tacmach.New in
let ci= (snd(fst cstr)) in
- let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+ let sigma = project gls in
+ let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in
let id=pf_get_new_id (Id.of_string "t") gls in
- mkLambda(Name id,intype,body)
+ sigma, mkLambda(Name id,intype,body)
(* generate an adhoc tactic following the proof tree *)
-let _M =mkMeta
-
let app_global f args k =
- Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
-
-let new_app_global f args k =
- Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
-
-let new_refine c = Proofview.V82.tactic (refine c)
+ Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args))
+
+let rec gen_holes env sigma t n accu =
+ if Int.equal n 0 then (sigma, List.rev accu)
+ else match EConstr.kind sigma t with
+ | Prod (_, u, t) ->
+ let (sigma, ev) = Evarutil.new_evar env sigma u in
+ let t = EConstr.Vars.subst1 ev t in
+ gen_holes env sigma t (pred n) (ev :: accu)
+ | _ -> assert false
+
+let app_global_with_holes f args n =
+ Proofview.Goal.enter begin fun gl ->
+ Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
+ Refine.refine ~typecheck:false begin fun sigma ->
+ let t = Tacmach.New.pf_get_type_of gl fc in
+ let t = Termops.prod_applist sigma t (Array.to_list args) in
+ let ans = mkApp (fc, args) in
+ let (sigma, holes) = gen_holes env sigma t n [] in
+ let ans = applist (ans, holes) in
+ let evdref = ref sigma in
+ let () = Typing.e_check env evdref ans concl in
+ (!evdref, ans)
+ end
+ end
let assert_before n c =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.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 }
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm)
+ (assert_before n c)
+ end
let refresh_type env evm ty =
Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
(Some false) env evm ty
let refresh_universes ty k =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let evm = Tacmach.New.project gl in
let evm, ty = refresh_type env evm ty in
- Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
- end }
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty)
+ end
+
+let constr_of_term c = EConstr.of_constr (constr_of_term c)
let rec proof_tac p : unit Proofview.tactic =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.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
- Ax c -> exact_check c
+ Ax c -> exact_check (EConstr.of_constr c)
| SymAx c ->
+ let c = EConstr.of_constr c in
let l=constr_of_term p.p_lhs and
r=constr_of_term p.p_rhs in
refresh_universes (type_of l) (fun typ ->
- new_app_global _sym_eq [|typ;r;l;c|] exact_check)
+ app_global _sym_eq [|typ;r;l;c|] exact_check)
| Refl t ->
let lr = constr_of_term t in
refresh_universes (type_of lr) (fun typ ->
- new_app_global _refl_equal [|typ;constr_of_term t|] exact_check)
+ app_global _refl_equal [|typ;constr_of_term t|] exact_check)
| Trans (p1,p2)->
let t1 = constr_of_term p1.p_lhs and
t2 = constr_of_term p1.p_rhs and
t3 = constr_of_term p2.p_rhs in
refresh_universes (type_of t2) (fun typ ->
- let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
- Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)])
+ let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
+ Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)])
| Congr (p1,p2)->
let tf1=constr_of_term p1.p_lhs
and tx1=constr_of_term p2.p_lhs
@@ -291,20 +322,20 @@ let rec proof_tac p : unit Proofview.tactic =
refresh_universes (type_of tf1) (fun typf ->
refresh_universes (type_of tx1) (fun typx ->
refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
- let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
+ let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
- let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
- let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
+ let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
+ let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
let prf =
- app_global _trans_eq
+ app_global_with_holes _trans_eq
[|typfx;
mkApp(tf1,[|tx1|]);
mkApp(tf2,[|tx1|]);
- mkApp(tf2,[|tx2|]);_M 2;_M 3|] in
- Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine))
- [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1);
+ mkApp(tf2,[|tx2|])|] 2 in
+ Tacticals.New.tclTHENS prf
+ [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
Tacticals.New.tclFIRST
- [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
+ [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
reflexivity;
Tacticals.New.tclZEROMSG
(Pp.str
@@ -316,96 +347,86 @@ let rec proof_tac p : unit Proofview.tactic =
let special=mkRel (1+nargs-argind) in
refresh_universes (type_of ti) (fun intype ->
refresh_universes (type_of default) (fun outtype ->
- let proj =
- Tacmach.New.of_old (build_projection intype cstr special default) gl
+ let sigma, proj =
+ 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)))
+ app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
+ Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (Tacticals.New.tclTHEN injt (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 { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
+ let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
let false_t=mkApp (c,[|mkVar hid|]) in
let k intype =
- let neweq= new_app_global _eq [|intype;tt1;tt2|] in
+ let neweq= app_global _eq [|intype;tt1;tt2|] in
Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
[proof_tac p; simplest_elim false_t]
in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
- 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 refine_exact_check c =
+ Proofview.Goal.enter begin fun gl ->
+ let evm, _ = Tacmach.New.pf_apply type_of gl c in
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (exact_check c)
+ end
let convert_to_goal_tac c t1 t2 p =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let k sort =
- let neweq= new_app_global _eq [|sort;tt1;tt2|] in
- let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
- let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+ let neweq= app_global _eq [|sort;tt1;tt2|] in
+ let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
+ let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
let identity=mkLambda (Name x,sort,mkRel 1) in
- let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+ 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)]
+ [proof_tac p; endt refine_exact_check]
in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
- end }
+ end
let convert_to_hyp_tac c1 t1 c2 t2 p =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.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 h = Tacmach.New.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 { enter = begin fun gl ->
- let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *)
+let discriminate_tac cstru p =
+ Proofview.Goal.enter begin fun gl ->
+ let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
let env = Proofview.Goal.env gl in
- let concl = Proofview.Goal.concl gl in
- let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
- let identity = Universes.constr_of_global (Lazy.force _I) in
- let trivial = Universes.constr_of_global (Lazy.force _True) in
let evm = Tacmach.New.project gl in
- let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
- let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm 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 cstru trivial concl) gl in
- let injt=app_global _f_equal
- [|intype;outtype;proj;t1;t2;mkVar hid|] in
- let endt k =
- injt (fun injt ->
- app_global _eq_rect
- [|outtype;trivial;pred;identity;concl;injt|] k) in
- let neweq=new_app_global _eq [|intype;t1;t2|] in
+ let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in
+ let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
+ let neweq=app_global _eq [|intype;lhs;rhs|] in
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 }
+ [proof_tac p; Equality.discrHyp hid])
+ end
(* wrap everything *)
-let build_term_to_complete uf meta pac =
+let build_term_to_complete uf pac =
let cinfo = get_constructor_info uf pac.cnode in
- let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
- let dummy_args = List.rev (List.init pac.arity meta) in
- let all_args = List.rev_append real_args dummy_args in
- applistc (mkConstructU cinfo.ci_constr) all_args
+ let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in
+ let (kn, u) = cinfo.ci_constr in
+ (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity)
let cc_tactic depth additionnal_terms =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Tacmach.New.project gl in
Coqlib.check_required_library Coqlib.logic_module_name;
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 state = make_prb gl depth additionnal_terms in
let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
let sol = execute true state in
let _ = debug (fun () -> Pp.str "Computation completed.") in
@@ -420,16 +441,17 @@ let cc_tactic depth additionnal_terms =
let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
discriminate_tac cstr p
| Incomplete ->
+ let open Glob_term in
let env = Proofview.Goal.env gl in
- let metacnt = ref 0 in
- let newmeta _ = incr metacnt; _M !metacnt in
- let terms_to_complete =
- List.map
- (build_term_to_complete uf newmeta)
- (epsilons uf) in
+ let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+ let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
+ let pr_missing (c, missing) =
+ let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
+ let holes = List.init missing (fun _ -> hole) in
+ Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
+ in
Feedback.msg_info
- (Pp.str "Goal is solvable by congruence but \
- some arguments are missing.");
+ (Pp.str "Goal is solvable by congruence but some arguments are missing.");
Feedback.msg_info
(Pp.str " Try " ++
hov 8
@@ -437,7 +459,7 @@ let cc_tactic depth additionnal_terms =
str "\"congruence with (" ++
prlist_with_sep
(fun () -> str ")" ++ spc () ++ str "(")
- (Termops.print_constr_env env)
+ pr_missing
terms_to_complete ++
str ")\","
end ++
@@ -448,20 +470,23 @@ let cc_tactic depth additionnal_terms =
let ta=term uf dis.lhs and tb=term uf dis.rhs in
match dis.rule with
Goal -> proof_tac p
- | Hyp id -> refute_tac id ta tb p
+ | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
| HeqG id ->
+ let id = EConstr.of_constr id in
convert_to_goal_tac id ta tb p
| HeqnH (ida,idb) ->
+ let ida = EConstr.of_constr ida in
+ let idb = EConstr.of_constr idb in
convert_to_hyp_tac ida ta idb tb p
- end }
+ end
-let cc_fail gls =
- errorlabstrm "Congruence" (Pp.str "congruence failed.")
+let cc_fail =
+ Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")
let congruence_tac depth l =
Tacticals.New.tclORELSE
(Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
- (Proofview.V82.tactic cc_fail)
+ cc_fail
(* Beware: reflexivity = constructor 1 = apply refl_equal
might be slow now, let's rather do something equivalent
@@ -475,31 +500,31 @@ let congruence_tac depth l =
*)
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 ->
+ Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
+ Proofview.Goal.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 })
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k term)
+ end
let f_equal =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
+ let sigma = Tacmach.New.project gl in
let cut_eq c1 c2 =
try (* type_of can raise an exception *)
Tacticals.New.tclTHENS
(mk_eq _eq c1 c2 Tactics.cut)
- [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)]
+ [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
Proofview.tclORELSE
- begin match kind_of_term concl with
- | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
- begin match kind_of_term t, kind_of_term t' with
+ begin match EConstr.kind sigma concl with
+ | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r ->
+ begin match EConstr.kind sigma t, EConstr.kind sigma t' with
| App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
let rec cuts i =
if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
@@ -510,7 +535,7 @@ let f_equal =
| _ -> Proofview.tclUNIT ()
end
begin function (e, info) -> match e with
- | Type_errors.TypeError _ -> Proofview.tclUNIT ()
+ | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT ()
| e -> Proofview.tclZERO ~info e
end
- end }
+ end
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 7c1d9f1c..a1bbcbc0 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -1,20 +1,20 @@
-
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Term
-open Proof_type
+open EConstr
val proof_tac: Ccproof.proof -> unit Proofview.tactic
val cc_tactic : int -> constr list -> unit Proofview.tactic
-val cc_fail : tactic
+val cc_fail : unit Proofview.tactic
val congruence_tac : int -> constr list -> unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 52a13511..fb013ac1 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -1,16 +1,16 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
+open Ltac_plugin
open Cctac
open Stdarg
-open Constrarg
DECLARE PLUGIN "cc_plugin"
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 14:08:00 +0000