aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/FunInd.v2
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/functional_principles_proofs.ml7
-rw-r--r--plugins/funind/functional_principles_proofs.mli1
-rw-r--r--plugins/funind/functional_principles_types.ml5
-rw-r--r--plugins/funind/functional_principles_types.mli3
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml1
-rw-r--r--plugins/funind/glob_term_to_relation.mli1
-rw-r--r--plugins/funind/glob_termops.ml1
-rw-r--r--plugins/funind/glob_termops.mli1
-rw-r--r--plugins/funind/indfun.ml7
-rw-r--r--plugins/funind/indfun.mli1
-rw-r--r--plugins/funind/indfun_common.ml3
-rw-r--r--plugins/funind/indfun_common.mli1
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--plugins/funind/merge.ml3
-rw-r--r--plugins/funind/recdef.ml5
-rw-r--r--plugins/funind/recdef.mli1
19 files changed, 17 insertions, 35 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
index e40aea7764..b8a05e5cc0 100644
--- a/plugins/funind/FunInd.v
+++ b/plugins/funind/FunInd.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index 64f43b8335..8b4dbbb45c 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ba46f78aa8..15ab396e31 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,4 +1,3 @@
-open API
open Printer
open CErrors
open Util
@@ -957,7 +956,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (fst (destConst evd f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let f_body = Option.get (Global.body_of_constant_body f_def) in
+ let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in
let f_body = EConstr.of_constr f_body in
let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1091,7 +1090,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let get_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
@@ -1382,7 +1381,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(* Proof of principles of general functions *)
-(* let hrec_id =
+(* let hrec_id = Recdef.hrec_id *)
(* and acc_inv_id = Recdef.acc_inv_id *)
(* and ltof_ref = Recdef.ltof_ref *)
(* and acc_rel = Recdef.acc_rel *)
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index d03fc475e0..64fbfaeedf 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,4 +1,3 @@
-open API
open Names
val prove_princ_for_struct :
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8ffd15f9fb..513fce2484 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,4 +1,3 @@
-open API
open Printer
open CErrors
open Util
@@ -407,7 +406,7 @@ let get_funs_constant mp dp =
function const ->
let find_constant_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
let body = Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
@@ -651,7 +650,7 @@ let build_case_scheme fa =
(* in *)
let funs =
let (_,f,_) = fa in
- try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+ try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
with Not_found ->
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_reference f) in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index e70ef23656..5a7ffe0590 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Term
open Misctypes
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1258c92868..16d9f200f3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "grammar/grammar.cma" i*)
-open API
-open Grammar_API
open Ltac_plugin
open Util
open Pp
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index db2af2be53..379c83b245 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,4 +1,3 @@
-open API
open Printer
open Pp
open Names
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 7ad7de0792..0cab5a6d35 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -1,4 +1,3 @@
-open API
open Names
(*
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 726a8203d7..7cb35838c7 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,4 +1,3 @@
-open API
open Pp
open Glob_term
open CErrors
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index b6d2c45437..99a258de98 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,4 +1,3 @@
-open API
open Names
open Glob_term
open Misctypes
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 35f0929587..863c9dc8d5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,4 +1,3 @@
-open API
open CErrors
open Util
open Names
@@ -593,7 +592,7 @@ and rebuild_nal aux bk bl' nal typ =
| na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } ->
if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
then
- let assum = CLocalAssum([na],bk',nal't) in
+ let assum = CLocalAssum([na],bk,nal't) in
let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
rebuild_nal
(assum::aux)
@@ -602,7 +601,7 @@ and rebuild_nal aux bk bl' nal typ =
nal
(CAst.make @@ CProdN(new_rest,typ'))
else
- let assum = CLocalAssum([na'],bk',nal't) in
+ let assum = CLocalAssum([na'],bk,nal't) in
let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
rebuild_nal
(assum::aux)
@@ -851,7 +850,7 @@ let make_graph (f_ref:global_reference) =
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom!"
- | Some body ->
+ | Some (body, _) ->
let env = Global.env () in
let sigma = Evd.from_env env in
let extern_body,extern_type =
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index fc7da6a338..7a60da44fb 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,4 +1,3 @@
-open API
open Misctypes
val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6fe6888f3d..f4f9ba2bbb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,4 +1,3 @@
-open API
open Names
open Pp
open Libnames
@@ -342,7 +341,7 @@ let pr_info f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr
- (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
+ (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index f7a9cedd73..5e425cd18a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,4 +1,3 @@
-open API
open Names
open Pp
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ef2590c8..8dea6c90f5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Ltac_plugin
open Declarations
open CErrors
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ba88563d3b..52a82b0e5e 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,6 @@
(* Merging of induction principles. *)
-open API
open Globnames
open Tactics
open Indfun_common
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8e12b239e8..d3eccb58d7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
module CVars = Vars
@@ -90,7 +89,7 @@ let type_of_const sigma t =
|_ -> assert false
let constr_of_global x =
- fst (Universes.unsafe_constr_of_global x)
+ fst (Global.constr_of_global_in_context (Global.env ()) x)
let constant sl s = constr_of_global (find_reference sl s)
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index f3d5e73320..63bbdbe7e3 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,4 +1,3 @@
-open API
(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
val tclUSER_if_not_mes :
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 12:48:04 +0000