aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml3
-rw-r--r--plugins/funind/functional_principles_proofs.ml5
-rw-r--r--plugins/funind/gen_principle.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml5
-rw-r--r--plugins/funind/glob_termops.ml7
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
7 files changed, 17 insertions, 11 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cca212f332..872f30135f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -351,7 +351,7 @@ let rec extract_type env sg db j c args =
| (Info, TypeScheme) ->
extract_type_app env sg db (r, type_sign env sg ty) args
| (Info, Default) -> Tunknown))
- | Cast _ | LetIn _ | Construct _ | Int _ -> assert false
+ | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
@@ -690,6 +690,7 @@ let rec extract_term env sg mle mlt c args =
let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in
extract_app env sg mle mlt extract_var args
| Int i -> assert (args = []); MLuint i
+ | Float _ -> assert false (* TODO: Implement primitive float for extraction *)
| Ind _ | Prod _ | Sort _ -> assert false
(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7be049269c..6db0a1119b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -692,13 +692,14 @@ let build_proof
end
| Cast(t,_,_) ->
build_proof do_finalize {dyn_infos with info = t} g
- | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ ->
do_finalize dyn_infos g
| App(_,_) ->
let f,args = decompose_app sigma dyn_infos.info in
begin
match EConstr.kind sigma f with
- | Int _ -> user_err Pp.(str "integer cannot be applied")
+ | Int _ -> user_err Pp.(str "integer cannot be applied")
+ | Float _ -> user_err Pp.(str "float cannot be applied")
| App _ -> assert false (* we have collected all the app in decompose_app *)
| Proj _ -> assert false (*FIXME*)
| Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ ->
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 0452665585..6add56dd5b 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -68,7 +68,7 @@ let is_rec names =
let check_id id names = Id.Set.mem id names in
let rec lookup names gt = match DAst.get gt with
| GVar(id) -> check_id id names
- | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false
+ | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ -> false
| GCast(b,_) -> lookup names b
| GRec _ -> CErrors.user_err (Pp.str "GRec not handled")
| GIf(b,_,lhs,rhs) ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7c17ecdba0..895b6a37ee 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -478,7 +478,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
let open CAst in
match DAst.get rt with
- | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ ->
+ | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ ->
(* do nothing (except changing type of course) *)
mk_result [] rt avoid
| GApp(_,_) ->
@@ -590,6 +590,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
| GInt _ -> user_err Pp.(str "Cannot apply an integer")
+ | GFloat _ -> user_err Pp.(str "Cannot apply a float")
end (* end of the application treatement *)
| GLambda(n,_,t,b) ->
@@ -1231,7 +1232,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
TODO: Find a valid way to deal with implicit arguments here!
*)
let rec compute_cst_params relnames params gt = DAst.with_val (function
- | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params
+ | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params
| GApp(f,args) ->
begin match DAst.get f with
| GVar relname' when Id.Set.mem relname' relnames ->
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8abccabae6..5f54bad598 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -115,6 +115,7 @@ let change_vars =
| GSort _ as x -> x
| GHole _ as x -> x
| GInt _ as x -> x
+ | GFloat _ as x -> x
| GCast(b,c) ->
GCast(change_vars mapping b,
Glob_ops.map_cast_type (change_vars mapping) c)
@@ -295,6 +296,7 @@ let rec alpha_rt excluded rt =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GSort _
| GInt _
+ | GFloat _
| GHole _ as rt -> rt
| GCast (b,c) ->
GCast(alpha_rt excluded b,
@@ -354,7 +356,7 @@ let is_free_in id =
| GHole _ -> false
| GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
| GCast (b,CastCoerce) -> is_free_in b
- | GInt _ -> false
+ | GInt _ | GFloat _ -> false
) x
and is_free_in_br {CAst.v=(ids,_,rt)} =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -447,6 +449,7 @@ let replace_var_by_term x_id term =
| GSort _
| GHole _ as rt -> rt
| GInt _ as rt -> rt
+ | GFloat _ as rt -> rt
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
Glob_ops.map_cast_type replace_var_by_pattern c)
@@ -529,7 +532,7 @@ let expand_as =
| PatCstr(_,patl,_) -> List.fold_left add_as map patl
in
let rec expand_as map = DAst.map (function
- | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt
+ | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ as rt -> rt
| GVar id as rt ->
begin
try
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 29356df81d..66ed1961ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -270,7 +270,7 @@ let check_not_nested env sigma forbidden e =
let rec check_not_nested e =
match EConstr.kind sigma e with
| Rel _ -> ()
- | Int _ -> ()
+ | Int _ | Float _ -> ()
| Var x ->
if Id.List.mem x forbidden
then user_err ~hdr:"Recdef.check_not_nested"
@@ -452,7 +452,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
| _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".")
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
- | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ ->
let new_continuation_tac =
jinfo.otherS () expr_info continuation_tac in
new_continuation_tac expr_info g
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4d7a04f5ee..9682487a22 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -319,7 +319,7 @@ let iter_constr_LR f c = match kind c with
for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
| Proj(_,a) -> f a
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _
- | Int _) -> ()
+ | Int _ | Float _) -> ()
(* The comparison used to determine which subterms matches is KEYED *)
(* CONVERSION. This looks for convertible terms that either have the same *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 04:16:11 +0000