summaryrefslogtreecommitdiff
path: root/plugins/dp
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/dp')
-rw-r--r--plugins/dp/Dp.v2
-rw-r--r--plugins/dp/dp.ml23
-rw-r--r--plugins/dp/g_dp.ml44
-rw-r--r--plugins/dp/test2.v2
-rw-r--r--plugins/dp/zenon.v2
5 files changed, 13 insertions, 20 deletions
diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v
index 5ddc4452..1b66c334 100644
--- a/plugins/dp/Dp.v
+++ b/plugins/dp/Dp.v
@@ -6,8 +6,6 @@ Require Export Classical.
(* Zenon *)
(* Copyright 2004 INRIA *)
-(* $Id: Dp.v 12337 2009-09-17 15:58:14Z glondu $ *)
-
Lemma zenon_nottrue :
(~True -> False).
Proof. tauto. Qed.
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index ceadd26e..837195e4 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -23,7 +23,6 @@ open Fol
open Names
open Nameops
open Namegen
-open Termops
open Coqlib
open Hipattern
open Libnames
@@ -37,7 +36,7 @@ let set_trace b = trace := b
let timeout = ref 10
let set_timeout n = timeout := n
-let (dp_timeout_obj,_) =
+let dp_timeout_obj : int -> obj =
declare_object
{(default_object "Dp_timeout") with
cache_function = (fun (_,x) -> set_timeout x);
@@ -45,7 +44,7 @@ let (dp_timeout_obj,_) =
let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
-let (dp_debug_obj,_) =
+let dp_debug_obj : bool -> obj =
declare_object
{(default_object "Dp_debug") with
cache_function = (fun (_,x) -> set_debug x);
@@ -53,7 +52,7 @@ let (dp_debug_obj,_) =
let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
-let (dp_trace_obj,_) =
+let dp_trace_obj : bool -> obj =
declare_object
{(default_object "Dp_trace") with
cache_function = (fun (_,x) -> set_trace x);
@@ -148,7 +147,7 @@ let fresh_var = function
env names, and returns the new variables together with the new
environment *)
let coq_rename_vars env vars =
- let avoid = ref (ids_of_named_context (Environ.named_context env)) in
+ let avoid = ref (Termops.ids_of_named_context (Environ.named_context env)) in
List.fold_right
(fun (na,t) (newvars, newenv) ->
let id = next_name_away na !avoid in
@@ -183,7 +182,7 @@ let decomp_type_lambdas env t =
let decompose_arrows =
let rec arrows_rec l c = match kind_of_term c with
- | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c
+ | Prod (_,t,c) when not (Termops.dependent (mkRel 1) c) -> arrows_rec (t :: l) c
| Cast (c,_,_) -> arrows_rec l c
| _ -> List.rev l, c
in
@@ -195,8 +194,8 @@ let rec eta_expanse t vars env i =
t, vars, env
else
match kind_of_term (Typing.type_of env Evd.empty t) with
- | Prod (n, a, b) when not (dependent (mkRel 1) b) ->
- let avoid = ids_of_named_context (Environ.named_context env) in
+ | Prod (n, a, b) when not (Termops.dependent (mkRel 1) b) ->
+ let avoid = Termops.ids_of_named_context (Environ.named_context env) in
let id = next_name_away n avoid in
let env' = Environ.push_named (id, None, a) env in
let t' = mkApp (t, [| mkVar id |]) in
@@ -469,7 +468,7 @@ and axiomatize_body env r id d = match r with
| VarRef _ ->
assert false
| ConstRef c ->
- begin match (Global.lookup_constant c).const_body with
+ begin match body_of_constant (Global.lookup_constant c) with
| Some b ->
let b = force b in
let axioms =
@@ -826,7 +825,7 @@ let prelude_files = ref ([] : string list)
let set_prelude l = prelude_files := l
-let (dp_prelude_obj,_) =
+let dp_prelude_obj : string list -> obj =
declare_object
{(default_object "Dp_prelude") with
cache_function = (fun (_,x) -> set_prelude x);
@@ -1088,7 +1087,7 @@ let dp_hint l =
in
List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
-let (dp_hint_obj,_) =
+let dp_hint_obj : reference list -> obj =
declare_object
{(default_object "Dp_hint") with
cache_function = (fun (_,l) -> dp_hint l);
@@ -1114,7 +1113,7 @@ let dp_predefined qid s =
with NotFO ->
msg_warning (str " ignored (not a first order declaration)")
-let (dp_predefined_obj,_) =
+let dp_predefined_obj : reference * string -> obj =
declare_object
{(default_object "Dp_predefined") with
cache_function = (fun (_,(id,s)) -> dp_predefined id s);
diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4
index fc957ea6..001ccce8 100644
--- a/plugins/dp/g_dp.ml4
+++ b/plugins/dp/g_dp.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_dp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Dp
TACTIC EXTEND Simplify
diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v
index 0940b135..ce660052 100644
--- a/plugins/dp/test2.v
+++ b/plugins/dp/test2.v
@@ -73,7 +73,7 @@ zenon.
Inductive IN (A:Set) : A -> list A -> Prop :=
| IN1 : forall x l, IN A x (x::l)
| IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
-Implicit Arguments IN [A].
+Arguments IN [A] _ _.
Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
zenon.
diff --git a/plugins/dp/zenon.v b/plugins/dp/zenon.v
index f2400a7f..89028c4f 100644
--- a/plugins/dp/zenon.v
+++ b/plugins/dp/zenon.v
@@ -1,6 +1,4 @@
(* Copyright 2004 INRIA *)
-(* $Id: zenon.v 11996 2009-03-20 01:22:58Z letouzey $ *)
-
Require Export Classical.
Lemma zenon_nottrue :
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 20:03:26 +0000