aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml32
-rw-r--r--plugins/firstorder/formula.mli18
-rw-r--r--plugins/firstorder/ground.ml2
-rw-r--r--plugins/firstorder/instances.ml4
-rw-r--r--plugins/firstorder/rules.ml12
-rw-r--r--plugins/firstorder/rules.mli8
-rw-r--r--plugins/firstorder/sequent.ml6
-rw-r--r--plugins/firstorder/unify.ml2
8 files changed, 43 insertions, 41 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 03a832e90e..430b549d9c 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -43,7 +43,7 @@ let rec nb_prod_after n c=
| _ -> 0
let construct_nhyps ind gls =
- let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+ let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in
let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
let hyp = nb_prod_after nparams in
Array.map hyp constr_types
@@ -67,10 +67,10 @@ let special_whd gl=
type kind_of_formula=
Arrow of constr*constr
- | False of inductive*constr list
- | And of inductive*constr list*bool
- | Or of inductive*constr list*bool
- | Exists of inductive*constr list
+ | False of pinductive*constr list
+ | And of pinductive*constr list*bool
+ | Or of pinductive*constr list*bool
+ | Exists of pinductive*constr list
| Forall of constr*constr
| Atom of constr
@@ -85,11 +85,11 @@ let kind_of_formula gl term =
|_->
match match_with_nodep_ind cciterm with
Some (i,l,n)->
- let ind=destInd i in
+ let ind,u=destInd i in
let (mib,mip) = Global.lookup_inductive ind in
let nconstr=Array.length mip.mind_consnames in
if Int.equal nconstr 0 then
- False(ind,l)
+ False((ind,u),l)
else
let has_realargs=(n>0) in
let is_trivial=
@@ -102,9 +102,9 @@ let kind_of_formula gl term =
Atom cciterm
else
if Int.equal nconstr 1 then
- And(ind,l,is_trivial)
+ And((ind,u),l,is_trivial)
else
- Or(ind,l,is_trivial)
+ Or((ind,u),l,is_trivial)
| _ ->
match match_with_sigma_type cciterm with
Some (i,l)-> Exists((destInd i),l)
@@ -186,19 +186,19 @@ type right_pattern =
type left_arrow_pattern=
LLatom
- | LLfalse of inductive*constr list
- | LLand of inductive*constr list
- | LLor of inductive*constr list
+ | LLfalse of pinductive*constr list
+ | LLand of pinductive*constr list
+ | LLor of pinductive*constr list
| LLforall of constr
- | LLexists of inductive*constr list
+ | LLexists of pinductive*constr list
| LLarrow of constr*constr*constr
type left_pattern=
Lfalse
- | Land of inductive
- | Lor of inductive
+ | Land of pinductive
+ | Lor of pinductive
| Lforall of metavariable*constr*bool
- | Lexists of inductive
+ | Lexists of pinductive
| LA of constr*left_arrow_pattern
type t={id:global_reference;
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 59b3633931..d12b106cc4 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -25,9 +25,9 @@ type ('a,'b) sum = Left of 'a | Right of 'b
type counter = bool -> metavariable
-val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
+val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
-val ind_hyps : int -> inductive -> constr list ->
+val ind_hyps : int -> pinductive -> constr list ->
Proof_type.goal Tacmach.sigma -> rel_context array
type atoms = {positive:constr list;negative:constr list}
@@ -49,19 +49,19 @@ type right_pattern =
type left_arrow_pattern=
LLatom
- | LLfalse of inductive*constr list
- | LLand of inductive*constr list
- | LLor of inductive*constr list
+ | LLfalse of pinductive*constr list
+ | LLand of pinductive*constr list
+ | LLor of pinductive*constr list
| LLforall of constr
- | LLexists of inductive*constr list
+ | LLexists of pinductive*constr list
| LLarrow of constr*constr*constr
type left_pattern=
Lfalse
- | Land of inductive
- | Lor of inductive
+ | Land of pinductive
+ | Lor of pinductive
| Lforall of metavariable*constr*bool
- | Lexists of inductive
+ | Lexists of pinductive
| LA of constr*left_arrow_pattern
type t={id: global_reference;
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 6c1709140b..e0f4fa95f3 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,7 +18,7 @@ let update_flags ()=
let predref=ref Names.Cpred.empty in
let f coe=
try
- let kn=destConst (Classops.get_coercion_value coe) in
+ let kn= fst (destConst (Classops.get_coercion_value coe)) in
predref:=Names.Cpred.add kn !predref
with DestKO -> ()
in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index fe22708a06..c6db6a49fb 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -101,6 +101,8 @@ let dummy_constr=mkMeta (-1)
let dummy_bvid=Id.of_string "x"
+let constr_of_global = Universes.constr_of_global
+
let mk_open_instance id gl m t=
let env=pf_env gl in
let evmap=Refiner.project gl in
@@ -128,7 +130,7 @@ let mk_open_instance id gl m t=
GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1)
| _-> anomaly (Pp.str "can't happen") in
let ntt=try
- Pretyping.understand evmap env (raux m rawt)
+ fst (Pretyping.understand evmap env (raux m rawt))(*FIXME*)
with e when Errors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
decompose_lam_n_assum m ntt
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 6d9af2bbfb..31a1e6cb00 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -53,7 +53,7 @@ let clear_global=function
VarRef id->clear [id]
| _->tclIDTAC
-
+let constr_of_global = Universes.constr_of_global
(* connection rules *)
let axiom_tac t seq=
@@ -117,14 +117,14 @@ let left_false_tac id=
(* We use this function for false, and, or, exists *)
-let ll_ind_tac ind largs backtrack id continue seq gl=
- let rcs=ind_hyps 0 ind largs gl in
+let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
+ let rcs=ind_hyps 0 indu largs gl in
let vargs=Array.of_list largs in
(* construire le terme H->B, le generaliser etc *)
let myterm i=
let rc=rcs.(i) in
let p=List.length rc in
- let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
+ let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in
let vars=Array.init p (fun j->mkRel (p-j)) in
let capply=mkApp ((lift p cstr),vars) in
let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
@@ -204,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq=
let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
let defined_connectives=lazy
- [AllOccurrences,EvalConstRef (destConst (constant "not"));
- AllOccurrences,EvalConstRef (destConst (constant "iff"))]
+ [AllOccurrences,EvalConstRef (fst (destConst (constant "not")));
+ AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))]
let normalize_evaluables=
onAllHypsAndConcl
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index bfebbaaf88..180f6f5da1 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -33,19 +33,19 @@ val or_tac : seqtac with_backtracking
val arrow_tac : seqtac with_backtracking
-val left_and_tac : inductive -> lseqtac with_backtracking
+val left_and_tac : pinductive -> lseqtac with_backtracking
-val left_or_tac : inductive -> lseqtac with_backtracking
+val left_or_tac : pinductive -> lseqtac with_backtracking
val left_false_tac : global_reference -> tactic
-val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking
+val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking
val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
val forall_tac : seqtac with_backtracking
-val left_exists_tac : inductive -> lseqtac with_backtracking
+val left_exists_tac : pinductive -> lseqtac with_backtracking
val ll_forall_tac : types -> lseqtac with_backtracking
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 72bde18f4b..c0e5c7e581 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -199,7 +199,7 @@ let expand_constructor_hints =
let extend_with_ref_list l seq gl=
let l = expand_constructor_hints l in
let f gr seq=
- let c=constr_of_global gr in
+ let c=Universes.constr_of_global gr in
let typ=(pf_type_of gl c) in
add_formula Hyp gr typ seq gl in
List.fold_right f l seq
@@ -210,10 +210,10 @@ let extend_with_auto_hints l seq gl=
let seqref=ref seq in
let f p_a_t =
match p_a_t.code with
- Res_pf (c,_) | Give_exact c
+ Res_pf (c,_) | Give_exact (c,_)
| Res_pf_THEN_trivial_fail (c,_) ->
(try
- let gr=global_of_constr c in
+ let gr = global_of_constr c in
let typ=(pf_type_of gl c) in
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 2556460f53..f7ee9fdad1 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -78,7 +78,7 @@ let unif t1 t2=
for i=0 to l-1 do
Queue.add (va.(i),vb.(i)) bige
done
- | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
+ | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2))
done;
assert false
(* this place is unreachable but needed for the sake of typing *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:21:01 +0000