aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-05-24 19:57:06 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-05-27 20:27:38 +0200
commit5cc13770ac2358d583b21f217b8c65d2d5abd850 (patch)
treeb4efff0efa2bb11c8586dbff2ef85d4d8d0328dd /plugins/funind
parent6841c6db48d57911d3886057e1ca47a5aa161ca7 (diff)
[coqlib] Move `Coqlib` to `library/`.
We move Coqlib to library in preparation for the late binding of Gallina-level references. Placing `Coqlib` in `library/` is convenient as some components such as pretyping need to depend on it. By moving we lose the ability to locate references by syntactic abbreviations, but IMHO it makes to require ML code to refer to a true constant instead of an abbreviation/notation. Unfortunately this change means that we break the `Coqlib` API (providing a compatibility function is not possible), however we do so for a good reason. The main changes are: - move `Coqlib` to `library/`. - remove reference -> term from `Coqlib`. In particular, clients will have different needs with regards to universes/evar_maps, so we force them to call the (not very safe) `Universes.constr_of_global` explicitly so the users are marked. - move late binding of impossible case from `Termops` to `pretying/Evarconv`. Remove hook. - `Coqlib.find_reference` doesn't support syntactic abbreviations anymore. - remove duplication of `Coqlib` code in `Program`. - remove duplication of `Coqlib` code in `Ltac.Rewrite`. - A special note about bug 5066 and commit 6e87877 . This case illustrates the danger of duplication in the code base; the solution chosen there was to transform the not-found anomaly into an error message, however the general policy was far from clear. The long term solution is indeed make `find_reference` emit `Not_found` and let the client handle the error maybe non-fatally. (so they can test for constants.
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml8
-rw-r--r--plugins/funind/indfun_common.ml3
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml6
4 files changed, 11 insertions, 8 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 55d361e3d..f8c7f98f6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -409,9 +409,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
let rec_pte_id = Id.of_string "Hrec"
let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
- let coq_False = EConstr.of_constr (Coqlib.build_coq_False ()) in
- let coq_True = EConstr.of_constr (Coqlib.build_coq_True ()) in
- let coq_I = EConstr.of_constr (Coqlib.build_coq_I ()) in
+ let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in
+ let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in
+ let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in
let rec scan_type context type_of_hyp : tactic =
if isLetIn sigma type_of_hyp then
let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -1596,7 +1596,7 @@ let prove_principle_for_gen
match !tcc_lemma_ref with
| Undefined -> error "No tcc proof !!"
| Value lemma -> EConstr.of_constr lemma
- | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ())
+ | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ())
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 257f02b70..90a082d1e 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -120,7 +120,8 @@ let def_of_const t =
|_ -> assert false
let coq_constant s =
- Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ Universes.constr_of_global @@
+ Coqlib.gen_reference_in_modules "RecursiveDefinition"
Coqlib.init_modules s;;
let find_reference sl s =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8c972cd7c..8eaa9b0f5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -546,7 +546,7 @@ and intros_with_rewrite_aux : tactic =
intros_with_rewrite
] g
end
- | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) ->
+ | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENSEQ[
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index eabad955e..00020609e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -54,7 +54,9 @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"]
let arith_Lt = ["Arith";"Lt"]
let coq_init_constant s =
- EConstr.of_constr (Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s)
+ EConstr.of_constr (
+ Universes.constr_of_global @@
+ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -1223,7 +1225,7 @@ let get_current_subgoals_types () =
exception EmptySubgoals
let build_and_l sigma l =
- let and_constr = Coqlib.build_coq_and () in
+ let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in
let conj_constr = coq_conj () in
let mk_and p1 p2 =
mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in