aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/pmisc.ml4
-rw-r--r--contrib/correctness/ptactic.ml3
-rw-r--r--contrib/correctness/ptyping.ml4
-rw-r--r--contrib/correctness/putil.ml11
-rw-r--r--contrib/correctness/pwp.ml5
-rw-r--r--contrib/extraction/extract_env.ml6
-rw-r--r--contrib/extraction/extraction.ml36
-rw-r--r--contrib/fourier/fourierR.ml16
-rw-r--r--contrib/interface/showproof.ml2
-rw-r--r--contrib/omega/coq_omega.ml12
-rw-r--r--contrib/ring/quote.ml4
-rw-r--r--contrib/romega/const_omega.ml12
-rw-r--r--contrib/xml/xmlcommand.ml6
13 files changed, 62 insertions, 59 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index c885242bd..936c39d56 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -146,8 +146,8 @@ let coq_constant d s =
make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
-let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
-let coq_false = mkMutConstruct (((bool_sp,0),2), [||])
+let coq_true = mkMutConstruct ((bool_sp,0),1)
+let coq_false = mkMutConstruct ((bool_sp,0),2)
let constant s =
let id = id_of_string s in
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 6a7a70cf3..d4c3494a8 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -122,6 +122,7 @@ let eq_pattern =
let (loop_ids : tactic) = fun gl ->
let rec arec hyps gl =
+ let env = pf_env gl in
let concl = pf_concl gl in
match hyps with
| [] -> tclIDTAC gl
@@ -135,7 +136,7 @@ let (loop_ids : tactic) = fun gl ->
match pf_matches gl eq_pattern (body_of_type a) with
| [_; _,varphi; _] when isVar varphi ->
let phi = destVar varphi in
- if occur_var phi concl then
+ if Environ.occur_var env phi concl then
tclTHEN (rewriteLR (mkVar id)) (arec al) gl
else
arec al gl
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index 29caf3107..de5d2da7d 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -107,10 +107,10 @@ let effect_app ren env f args =
* Also returns its variables *)
let state_coq_ast sign a =
+ let env = Global.env_of_context sign in
let j =
- let env = Global.env_of_context sign in
reraise_with_loc (Ast.loc a) (judgment_of_rawconstr Evd.empty env) a in
- let ids = global_vars j.uj_val in
+ let ids = global_vars env j.uj_val in
j.uj_val, j.uj_type, ids
(* [is_pure p] tests wether the program p is an expression or not. *)
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index e227a4459..73d1778ac 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Term
open Pattern
+open Environ
open Pmisc
open Ptype
@@ -61,10 +62,10 @@ let is_mutable_in_env env id =
let now_vars env c =
Util.map_succeed
(function id -> if is_mutable_in_env env id then id else failwith "caught")
- (global_vars c)
+ (global_vars (Global.env()) c)
let make_before_after c =
- let ids = global_vars c in
+ let ids = global_vars (Global.env()) c in
let al =
Util.map_succeed
(function id ->
@@ -98,18 +99,18 @@ let make_assoc_list ren env on_prime ids =
[] ids
let apply_pre ren env c =
- let ids = global_vars c.p_value in
+ let ids = global_vars (Global.env()) c.p_value in
let al = make_assoc_list ren env current_var ids in
{ p_assert = c.p_assert; p_name = c.p_name;
p_value = subst_in_constr al c.p_value }
let apply_assert ren env c =
- let ids = global_vars c.a_value in
+ let ids = global_vars (Global.env()) c.a_value in
let al = make_assoc_list ren env current_var ids in
{ a_name = c.a_name; a_value = subst_in_constr al c.a_value }
let apply_post ren env before c =
- let ids = global_vars c.a_value in
+ let ids = global_vars (Global.env()) c.a_value in
let al =
make_assoc_list ren env (fun r uid -> var_at_date r before uid) ids in
{ a_name = c.a_name; a_value = subst_in_constr al c.a_value }
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index b00f5c38f..1381bdf92 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -13,6 +13,7 @@
open Util
open Names
open Term
+open Environ
open Pmisc
open Ptype
@@ -53,7 +54,7 @@ let update_post env top ef c =
l
else
l)
- [] (global_vars c)
+ [] (global_vars (Global.env()) c)
in
subst_in_constr al c
@@ -110,7 +111,7 @@ let create_bool_post c =
let is_bool = function
| TypePure c ->
(match kind_of_term (strip_outer_cast c) with
- | IsMutInd (op,_) -> Global.string_of_global (IndRef op) = "bool"
+ | IsMutInd op -> Global.string_of_global (IndRef op) = "bool"
| _ -> false)
| _ -> false
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index cd6160b2a..93e8d4cf5 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -138,9 +138,9 @@ let _ =
let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
match kind_of_term c with
(* If it is a global reference, then output the declaration *)
- | IsConst (sp,_) -> extract_reference (ConstRef sp)
- | IsMutInd (ind,_) -> extract_reference (IndRef ind)
- | IsMutConstruct (cs,_) -> extract_reference (ConstructRef cs)
+ | IsConst sp -> extract_reference (ConstRef sp)
+ | IsMutInd ind -> extract_reference (IndRef ind)
+ | IsMutConstruct cs -> extract_reference (ConstructRef cs)
(* Otherwise, output the ML type or expression *)
| _ ->
match extract_constr (Global.env()) [] c with
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 8f70b560f..f5b28598c 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -262,7 +262,7 @@ type inductive_extraction_result =
| Iprop
let inductive_extraction_table =
- ref (Gmap.empty : (inductive_path, inductive_extraction_result) Gmap.t)
+ ref (Gmap.empty : (inductive, inductive_extraction_result) Gmap.t)
let add_inductive_extraction i e =
inductive_extraction_table := Gmap.add i e !inductive_extraction_table
@@ -274,7 +274,7 @@ type constructor_extraction_result =
| Cprop
let constructor_extraction_table =
- ref (Gmap.empty : (constructor_path, constructor_extraction_result) Gmap.t)
+ ref (Gmap.empty : (constructor, constructor_extraction_result) Gmap.t)
let add_constructor_extraction c e =
constructor_extraction_table := Gmap.add c e !constructor_extraction_table
@@ -358,13 +358,13 @@ and extract_type_rec_info env c vl args =
| None ->
let id = id_of_name (fst (lookup_rel_type n env)) in
Tmltype (Tvar id, [], vl))
- | IsConst (sp,a) when args = [] && is_ml_extraction (ConstRef sp) ->
+ | IsConst sp when args = [] && is_ml_extraction (ConstRef sp) ->
Tmltype (Tglob (ConstRef sp), [], vl)
- | IsConst (sp,a) when is_axiom sp ->
+ | IsConst sp when is_axiom sp ->
let id = next_ident_away (basename sp) vl in
Tmltype (Tvar id, [], id :: vl)
- | IsConst (sp,a) ->
- let t = constant_type env none (sp,a) in
+ | IsConst sp ->
+ let t = constant_type env none sp in
if is_arity env none t then
(match extract_constant sp with
| Emltype (Miniml.Tarity,_,_) -> Tarity
@@ -375,9 +375,9 @@ and extract_type_rec_info env c vl args =
else
(* We can't keep as ML type abbreviation a CIC constant *)
(* which type is not an arity: we reduce this constant. *)
- let cvalue = constant_value env (sp,a) in
+ let cvalue = constant_value env sp in
extract_type_rec_info env (applist (cvalue, args)) vl []
- | IsMutInd (spi,_) ->
+ | IsMutInd spi ->
(match extract_inductive spi with
|Iml (si,vli) ->
extract_type_app env (IndRef spi,si,vli) vl args
@@ -520,11 +520,11 @@ and extract_term_info_with_type env ctx c t =
extract_term_info env' (false :: ctx) c2)
| IsRel n ->
MLrel (renum_db ctx n)
- | IsConst (sp,_) ->
+ | IsConst sp ->
MLglob (ConstRef sp)
| IsApp (f,a) ->
extract_app env ctx f a
- | IsMutConstruct (cp,_) ->
+ | IsMutConstruct cp ->
abstract_constructor cp
| IsMutCase ((_,(ip,_,_,_,_)),_,c,br) ->
extract_case env ctx ip c br
@@ -577,7 +577,7 @@ and abstract_constructor cp =
(* Extraction of a case *)
and extract_case env ctx ip c br =
- let mis = Global.lookup_mind_specif (ip,[||]) in
+ let mis = Global.lookup_mind_specif ip in
let ni = Array.map List.length (mis_recarg mis) in
(* [ni]: number of arguments without parameters in each branch *)
(* [br]: bodies of each branch (in functional form) *)
@@ -756,7 +756,7 @@ and extract_constructor (((sp,_),_) as c) =
and is_singleton_inductive (sp,_) =
let mib = Global.lookup_mind sp in
(mib.mind_ntypes = 1) &&
- let mis = build_mis ((sp,0),[||]) mib in
+ let mis = build_mis (sp,0) mib in
(mis_nconstr mis = 1) &&
match extract_constructor ((sp,0),1) with
| Cml ([mlt],_,_)-> (try parse_ml_type sp mlt; true with Found_sp -> false)
@@ -775,7 +775,7 @@ and extract_mib sp =
let genv = Global.env () in
(* Everything concerning parameters.
We do that first, since they are common to all the [mib]. *)
- let mis = build_mis ((sp,0),[||]) mib in
+ let mis = build_mis (sp,0) mib in
let nb = mis_nparams mis in
let rb = mis_params_ctxt mis in
let env = push_rels rb genv in
@@ -789,7 +789,7 @@ and extract_mib sp =
let vl0 = iterate_for 0 (mib.mind_ntypes - 1)
(fun i vl ->
let ip = (sp,i) in
- let mis = build_mis (ip,[||]) mib in
+ let mis = build_mis ip mib in
if (mis_sort mis) = (Prop Null) then begin
add_inductive_extraction ip Iprop; vl
end else begin
@@ -808,7 +808,7 @@ and extract_mib sp =
iterate_for 0 (mib.mind_ntypes - 1)
(fun i vl ->
let ip = (sp,i) in
- let mis = build_mis (ip,[||]) mib in
+ let mis = build_mis ip mib in
if mis_sort mis = Prop Null then begin
for j = 1 to mis_nconstr mis do
add_constructor_extraction (ip,j) Cprop
@@ -832,7 +832,7 @@ and extract_mib sp =
(* Third pass: we update the type variables list in the inductives table *)
for i = 0 to mib.mind_ntypes-1 do
let ip = (sp,i) in
- let mis = build_mis (ip,[||]) mib in
+ let mis = build_mis ip mib in
match lookup_inductive_extraction ip with
| Iprop -> ()
| Iml (s,l) -> add_inductive_extraction ip (Iml (s,vl@l));
@@ -840,7 +840,7 @@ and extract_mib sp =
(* Fourth pass: we update also in the constructors table *)
for i = 0 to mib.mind_ntypes-1 do
let ip = (sp,i) in
- let mis = build_mis (ip,[||]) mib in
+ let mis = build_mis ip mib in
for j = 1 to mis_nconstr mis do
let cp = (ip,j) in
match lookup_constructor_extraction cp with
@@ -880,7 +880,7 @@ and extract_inductive_declaration sp =
iterate_for (1 - mib.mind_ntypes) 0
(fun i acc ->
let ip = (sp,-i) in
- let mis = build_mis (ip,[||]) mib in
+ let mis = build_mis ip mib in
match lookup_inductive_extraction ip with
| Iprop -> acc
| Iml (_,vl) ->
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 49706bbd3..652a96910 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -76,7 +76,7 @@ let pf_parse_constr gl s =
let rec string_of_constr c =
match kind_of_term c with
IsCast (c,t) -> string_of_constr c
- |IsConst (c,l) -> string_of_path c
+ |IsConst c -> string_of_path c
|IsVar(c) -> string_of_id c
| _ -> "not_of_constant"
;;
@@ -86,7 +86,7 @@ let rec rational_of_constr c =
| IsCast (c,t) -> (rational_of_constr c)
| IsApp (c,args) ->
(match kind_of_term c with
- IsConst (c,l) ->
+ IsConst c ->
(match (string_of_path c) with
"Coq.Reals.Rdefinitions.Ropp" ->
rop (rational_of_constr args.(0))
@@ -106,7 +106,7 @@ let rec rational_of_constr c =
(rational_of_constr args.(1))
| _ -> failwith "not a rational")
| _ -> failwith "not a rational")
- | IsConst (c,l) ->
+ | IsConst c ->
(match (string_of_path c) with
"Coq.Reals.Rdefinitions.R1" -> r1
|"Coq.Reals.Rdefinitions.R0" -> r0
@@ -120,7 +120,7 @@ let rec flin_of_constr c =
| IsCast (c,t) -> (flin_of_constr c)
| IsApp (c,args) ->
(match kind_of_term c with
- IsConst (c,l) ->
+ IsConst c ->
(match (string_of_path c) with
"Coq.Reals.Rdefinitions.Ropp" ->
flin_emult (rop r1) (flin_of_constr args.(0))
@@ -152,7 +152,7 @@ let rec flin_of_constr c =
(rinv b)))
|_->assert false)
|_ -> assert false)
- | IsConst (c,l) ->
+ | IsConst c ->
(match (string_of_path c) with
"Coq.Reals.Rdefinitions.R1" -> flin_one ()
|"Coq.Reals.Rdefinitions.R0" -> flin_zero ()
@@ -187,7 +187,7 @@ let ineq1_of_constr (h,t) =
let t1= args.(0) in
let t2= args.(1) in
(match kind_of_term f with
- IsConst (c,l) ->
+ IsConst c ->
(match (string_of_path c) with
"Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
htype="Rlt";
@@ -218,13 +218,13 @@ let ineq1_of_constr (h,t) =
(flin_of_constr t1);
hstrict=false}]
|_->assert false)
- | IsMutInd ((sp,i),l) ->
+ | IsMutInd (sp,i) ->
(match (string_of_path sp) with
"Coq.Init.Logic_Type.eqT" -> let t0= args.(0) in
let t1= args.(1) in
let t2= args.(2) in
(match (kind_of_term t0) with
- IsConst (c,l) ->
+ IsConst c ->
(match (string_of_path c) with
"Coq.Reals.Rdefinitions.R"->
[{hname=h;
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index aa158f841..50aebb917 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -737,7 +737,7 @@ let rec nsortrec vl x =
| IsMutCase(_,x,t,a)
-> nsortrec vl x
| IsCast(x,t)-> nsortrec vl t
- | IsConst((c,_)) -> nsortrec vl (lookup_constant c vl).const_type
+ | IsConst c -> nsortrec vl (lookup_constant c vl).const_type
| _ -> nsortrec vl (type_of vl Evd.empty x)
;;
let nsort x =
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index d56f92cfa..d12f868ac 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -177,9 +177,9 @@ let dest_const_apply t =
let f,args = get_applist t in
let ref =
match kind_of_term f with
- | IsConst (sp,_) -> ConstRef sp
- | IsMutConstruct (csp,_) -> ConstructRef csp
- | IsMutInd (isp,_) -> IndRef isp
+ | IsConst sp -> ConstRef sp
+ | IsMutConstruct csp -> ConstructRef csp
+ | IsMutInd isp -> IndRef isp
| _ -> raise Destruct
in
basename (Global.sp_of_global ref), args
@@ -193,12 +193,12 @@ type result =
let destructurate t =
let c, args = get_applist t in
match kind_of_term c, args with
- | IsConst (sp,_), args ->
+ | IsConst sp, args ->
Kapp (string_of_id (basename (Global.sp_of_global (ConstRef sp))),args)
- | IsMutConstruct (csp,_) , args ->
+ | IsMutConstruct csp , args ->
Kapp (string_of_id (basename (Global.sp_of_global (ConstructRef csp))),
args)
- | IsMutInd (isp,_), args ->
+ | IsMutInd isp, args ->
Kapp (string_of_id (basename (Global.sp_of_global (IndRef isp))),args)
| IsVar id,[] -> Kvar(string_of_id id)
| IsProd (Anonymous,typ,body), [] -> Kimp(typ,body)
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 10ca06b78..b87ec5861 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -200,9 +200,9 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
let compute_lhs typ i nargsi =
match kind_of_term typ with
- | IsMutInd((sp,0),args) ->
+ | IsMutInd(sp,0) ->
let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
- mkApp (mkMutConstruct (((sp,0),i+1), args), argsi)
+ mkApp (mkMutConstruct ((sp,0),i+1), argsi)
| _ -> i_can't_do_that ()
(*s This function builds the pattern from the RHS. Recursive calls are
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 37fb01a4c..173c44356 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -18,14 +18,14 @@ type result =
let destructurate t =
let c, args = Reduction.whd_stack t in
match Term.kind_of_term c, args with
- | Term.IsConst (sp,_), args ->
+ | Term.IsConst sp, args ->
Kapp (Names.string_of_id
(Names.basename (Global.sp_of_global (Term.ConstRef sp))),args)
- | Term.IsMutConstruct (csp,_) , args ->
+ | Term.IsMutConstruct csp , args ->
Kapp (Names.string_of_id
(Names.basename (Global.sp_of_global (Term.ConstructRef csp))),
args)
- | Term.IsMutInd (isp,_), args ->
+ | Term.IsMutInd isp, args ->
Kapp (Names.string_of_id
(Names.basename (Global.sp_of_global (Term.IndRef isp))),args)
| Term.IsVar id,[] -> Kvar(Names.string_of_id id)
@@ -40,9 +40,9 @@ let dest_const_apply t =
let f,args = Reduction.whd_stack t in
let ref =
match Term.kind_of_term f with
- | Term.IsConst (sp,_) -> Term.ConstRef sp
- | Term.IsMutConstruct (csp,_) -> Term.ConstructRef csp
- | Term.IsMutInd (isp,_) -> Term.IndRef isp
+ | Term.IsConst sp -> Term.ConstRef sp
+ | Term.IsMutConstruct csp -> Term.ConstructRef csp
+ | Term.IsMutInd isp -> Term.IndRef isp
| _ -> raise Destruct
in
Names.basename (Global.sp_of_global ref), args
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index f4b75583c..d79e43813 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -414,16 +414,16 @@ let print_term inner_types l env csr =
(fun x i -> [< (term_display idradix false l env x); i >]) t [<>])
>]
)
- | T.IsConst (sp,_) ->
+ | T.IsConst sp ->
X.xml_empty "CONST"
(add_sort_attribute false
["uri",(uri_of_path sp Constant) ; "id", next_id])
- | T.IsMutInd ((sp,i),_) ->
+ | T.IsMutInd (sp,i) ->
X.xml_empty "MUTIND"
["uri",(uri_of_path sp Inductive) ;
"noType",(string_of_int i) ;
"id", next_id]
- | T.IsMutConstruct (((sp,i),j),_) ->
+ | T.IsMutConstruct ((sp,i),j) ->
X.xml_empty "MUTCONSTRUCT"
(add_sort_attribute false
["uri",(uri_of_path sp Inductive) ;
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-14 11:55:18 +0000