aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml4
-rw-r--r--plugins/firstorder/formula.mli4
-rw-r--r--plugins/firstorder/g_ground.mlg9
-rw-r--r--plugins/firstorder/ground.ml8
-rw-r--r--plugins/firstorder/ground.mli4
-rw-r--r--plugins/firstorder/instances.ml37
-rw-r--r--plugins/firstorder/instances.mli4
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/firstorder/sequent.ml40
-rw-r--r--plugins/firstorder/sequent.mli4
-rw-r--r--plugins/firstorder/unify.ml4
-rw-r--r--plugins/firstorder/unify.mli4
13 files changed, 66 insertions, 64 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 38dd8992bc..c76287d288 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index b8a619d1e6..a630e7f6e9 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 8946587a02..49e4c91182 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -36,7 +36,6 @@ let ground_depth=ref 3
let ()=
let gdopt=
{ optdepr=false;
- optname="Firstorder Depth";
optkey=["Firstorder";"Depth"];
optread=(fun ()->Some !ground_depth);
optwrite=
@@ -48,7 +47,7 @@ let ()=
let default_intuition_tac =
- let tac _ _ = Auto.h_auto None [] None in
+ let tac _ _ = Auto.h_auto None [] (Some []) 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 |];
@@ -88,7 +87,7 @@ let gen_ground_tac flag taco ids bases =
Proofview.Goal.enter begin fun gl ->
let seq=empty_seq !ground_depth in
let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
- let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
+ let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in
tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
end
in
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 2f26226f4e..7a9026a6ca 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -18,11 +18,11 @@ open Tacticals.New
let update_flags ()=
let open TransparentState in
- let f accu coe = match coe.Classops.coe_value with
+ let f accu coe = match coe.Coercionops.coe_value with
| Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
| _ -> accu
in
- let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
+ let flags = List.fold_left f TransparentState.full (Coercionops.coercions ()) in
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 67735fc2a3..0b9699eb41 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e131cad7da..834e4251d3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -100,25 +100,28 @@ let rec collect_quantified sigma seq=
let dummy_bvid=Id.of_string "x"
-let mk_open_instance env evmap id idc m t =
- let var_id=
- if id==dummy_id then dummy_bvid else
- let typ=Typing.unsafe_type_of env evmap idc in
+let mk_open_instance env sigma id idc m t =
+ let var_id =
+ (* XXX why physical equality? *)
+ if id == dummy_id then dummy_bvid else
+ let typ = Retyping.get_type_of env sigma idc in
(* since we know we will get a product,
reduction is not too expensive *)
- let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
+ let (nam,_,_) = destProd sigma (whd_all env sigma typ) in
match nam.Context.binder_name 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 env evmap decls =
- if Int.equal n 0 then evmap, decls else
- let nid=(fresh_id_in_env avoid var_id env) in
- let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+ | 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 env sigma decls =
+ if Int.equal n 0 then sigma, decls else
+ let nid = fresh_id_in_env avoid var_id env in
+ let (sigma, (c, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
- aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
- let evmap, decls = aux m Id.Set.empty env evmap [] in
- (evmap, decls, revt)
+ aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) sigma (decl::decls)
+ in
+ let sigma, decls = aux m Id.Set.empty env sigma [] in
+ (sigma, decls, revt)
(* tactics *)
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index be31a2d7a1..c0f4c78ff3 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 3413db930b..e68e3431c0 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 62d4354953..ee0c6d0be7 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 7d84ee6851..7bf13fd25b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -204,28 +204,28 @@ let extend_with_ref_list env sigma l seq =
open Hints
let extend_with_auto_hints env sigma l seq =
- let seqref=ref seq in
- let f p_a_t =
+ let f (seq,sigma) p_a_t =
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, _) = Termops.global_of_constr sigma c in
- let typ=(Typing.unsafe_type_of env sigma c) in
- seqref:=add_formula env sigma Hint gr typ !seqref
- with Not_found->())
- | _-> () in
- let g _ _ l = List.iter f l in
- let h dbname=
- let hdb=
+ | Res_pf (c,_) | Give_exact (c,_)
+ | Res_pf_THEN_trivial_fail (c,_) ->
+ let (c, _, _) = c in
+ (match EConstr.destRef sigma c with
+ | exception Constr.DestKO -> seq, sigma
+ | gr, _ ->
+ let sigma, typ = Typing.type_of env sigma c in
+ add_formula env sigma Hint gr typ seq, sigma)
+ | _ -> seq, sigma
+ in
+ let h acc dbname =
+ let hdb =
try
searchtable_map dbname
with Not_found->
- user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in
- Hint_db.iter g hdb in
- List.iter h l;
- !seqref, sigma (*FIXME: forgetting about universes*)
+ user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database"))
+ in
+ Hint_db.fold (fun _ _ l acc -> List.fold_left f acc l) hdb acc
+ in
+ List.fold_left h (seq,sigma) l
let print_cmap map=
let print_entry c l s=
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 2e262fd996..3a5da6ad14 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 6fa831fda9..e58e80116d 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 a782900e05..71e786eb90 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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-05-02 08:01:50 +0000