aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml13
-rw-r--r--plugins/firstorder/formula.mli2
-rw-r--r--plugins/firstorder/g_ground.mlg4
-rw-r--r--plugins/firstorder/ground.ml5
-rw-r--r--plugins/firstorder/ground.mli2
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/firstorder/instances.mli2
-rw-r--r--plugins/firstorder/rules.ml7
-rw-r--r--plugins/firstorder/rules.mli2
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/firstorder/sequent.mli2
-rw-r--r--plugins/firstorder/unify.ml2
-rw-r--r--plugins/firstorder/unify.mli2
13 files changed, 23 insertions, 26 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 56b3dc97cf..fb363b9393 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -15,7 +15,6 @@ open EConstr
open Vars
open Util
open Declarations
-open Globnames
module RelDecl = Context.Rel.Declaration
@@ -82,13 +81,13 @@ let pop t = Vars.lift (-1) t
let kind_of_formula env sigma term =
let normalize = special_nf env sigma in
let cciterm = special_whd env sigma term in
- match match_with_imp_term sigma cciterm with
+ match match_with_imp_term env sigma cciterm with
Some (a,b)-> Arrow (a, pop b)
|_->
- match match_with_forall_term sigma cciterm with
+ match match_with_forall_term env sigma cciterm with
Some (_,a,b)-> Forall (a, b)
|_->
- match match_with_nodep_ind sigma cciterm with
+ match match_with_nodep_ind env sigma cciterm with
Some (i,l,n)->
let ind,u=EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
@@ -111,7 +110,7 @@ let kind_of_formula env sigma term =
else
Or((ind,u),l,is_trivial)
| _ ->
- match match_with_sigma_type sigma cciterm with
+ match match_with_sigma_type env sigma cciterm with
Some (i,l)->
let (ind, u) = EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
@@ -124,7 +123,7 @@ type side = Hyp | Concl | Hint
let no_atoms = (false,{positive=[];negative=[]})
-let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
+let dummy_id=GlobRef.VarRef (Id.of_string "_") (* "_" cannot be parsed *)
let build_atoms env sigma metagen side cciterm =
let trivial =ref false
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index e2c6f1c4b1..dc422fa284 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index ea86a4b514..35cd10a1ff 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -83,7 +83,7 @@ END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> {
- Feedback.msg_info
+ Feedback.msg_notice
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
END
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 6a80525200..e134562702 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -15,12 +15,11 @@ open Rules
open Instances
open Tacmach.New
open Tacticals.New
-open Globnames
let update_flags ()=
let open TransparentState in
let f accu coe = match coe.Classops.coe_value with
- | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+ | 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
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 958fc4cf18..67735fc2a3 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 1c9ab2e3bd..eff0db5bf4 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 9f9ade3aab..be31a2d7a1 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 7f06ab6777..79386f7ac9 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -20,7 +20,6 @@ open Proofview.Notations
open Termops
open Formula
open Sequent
-open Globnames
module NamedDecl = Context.Named.Declaration
@@ -48,7 +47,7 @@ let wrap n b continue seq =
List.exists (occur_var_in_decl env sigma id) ctx then
(aux (i-1) q (nd::ctx))
else
- add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
+ add_formula env sigma Hyp (GlobRef.VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
let seq1=aux n nc [] in
let seq2=if b then
add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
@@ -56,7 +55,7 @@ let wrap n b continue seq =
end
let clear_global=function
- VarRef id-> clear [id]
+ | GlobRef.VarRef id-> clear [id]
| _->tclIDTAC
(* connection rules *)
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 97bc992b26..62d4354953 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 01b18e2f30..e53412383c 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -188,7 +188,7 @@ let empty_seq depth=
let expand_constructor_hints =
List.map_append (function
| GlobRef.IndRef ind ->
- List.init (Inductiveops.nconstructors ind)
+ List.init (Inductiveops.nconstructors (Global.env()) ind)
(fun i -> GlobRef.ConstructRef (ind,i+1))
| gr ->
[gr])
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 709b278ec4..724e1abcc4 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 0c958ddee3..35b64ccb8f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index ed35500f5f..a782900e05 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:37:12 +0000