aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/firstorder/formula.ml8
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/funind/g_indfun.mlg6
-rw-r--r--plugins/funind/glob_term_to_relation.ml6
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/funind/indfun.ml91
-rw-r--r--plugins/funind/plugin_base.dune2
-rw-r--r--plugins/ltac/g_class.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg5
-rw-r--r--plugins/ltac/rewrite.ml66
-rw-r--r--plugins/ltac/tacsubst.ml6
-rw-r--r--plugins/ltac/tauto.ml18
-rw-r--r--plugins/setoid_ring/RealField.v5
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrequality.ml6
-rw-r--r--plugins/ssr/ssrparser.mlg16
-rw-r--r--plugins/ssr/ssrvernac.mlg4
-rw-r--r--plugins/ssr/ssrview.ml2
-rw-r--r--plugins/syntax/numeral.ml45
-rw-r--r--plugins/syntax/r_syntax.ml71
22 files changed, 227 insertions, 142 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 50fc2448fc..0e3b9fc2b6 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -67,7 +67,7 @@ let rec decompose_term env sigma t=
let canon_mind = MutInd.make1 (MutInd.canonical mind) in
let canon_ind = canon_mind,i_ind in
let (oib,_)=Global.lookup_inductive (canon_ind) in
- let nargs=constructor_nallargs_env env (canon_ind,i_con) in
+ let nargs=constructor_nallargs env (canon_ind,i_con) in
Constructor {ci_constr= ((canon_ind,i_con),u);
ci_arity=nargs;
ci_nhyps=nargs-oib.mind_nparams}
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c9cfd74362..9db7c8d8d3 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
(* [br]: bodies of each branch (in functional form) *)
(* [ni]: number of arguments without parameters in each branch *)
- let ni = constructors_nrealargs_env env ip in
+ let ni = constructors_nrealargs env ip in
let br_size = Array.length br in
assert (Int.equal (Array.length ni) br_size);
if Int.equal br_size 0 then begin
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 56b3dc97cf..4b7bc707d6 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -82,13 +82,13 @@ let pop t = Vars.lift (-1) t
let kind_of_formula env sigma term =
let normalize = special_nf env sigma in
let cciterm = special_whd env sigma term in
- match match_with_imp_term sigma cciterm with
+ match match_with_imp_term env sigma cciterm with
Some (a,b)-> Arrow (a, pop b)
|_->
- match match_with_forall_term sigma cciterm with
+ match match_with_forall_term env sigma cciterm with
Some (_,a,b)-> Forall (a, b)
|_->
- match match_with_nodep_ind sigma cciterm with
+ match match_with_nodep_ind env sigma cciterm with
Some (i,l,n)->
let ind,u=EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
@@ -111,7 +111,7 @@ let kind_of_formula env sigma term =
else
Or((ind,u),l,is_trivial)
| _ ->
- match match_with_sigma_type sigma cciterm with
+ match match_with_sigma_type env sigma cciterm with
Some (i,l)->
let (ind, u) = EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 01b18e2f30..9f2ceb2c28 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -188,7 +188,7 @@ let empty_seq depth=
let expand_constructor_hints =
List.map_append (function
| GlobRef.IndRef ind ->
- List.init (Inductiveops.nconstructors ind)
+ List.init (Inductiveops.nconstructors (Global.env()) ind)
(fun i -> GlobRef.ConstructRef (ind,i+1))
| gr ->
[gr])
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 4e8cf80ed2..a3973732ad 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -179,8 +179,10 @@ let () =
VERNAC COMMAND EXTEND Function
| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
=> { let hard = List.exists (function
- | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true
- | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
+ | _,((_,(Some { CAst.v = CMeasureRec _ }
+ | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
+ | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
+ | _,((_,None,_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
(Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 275b58f0aa..45a4e61846 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl =
Impargs.implicits_of_global constructref
in
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
construct
in
@@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl =
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
in
- cases_pattern_of_glob_constr Anonymous pat_as_term
+ cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
)
ind.Declarations.mind_consnames
@@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function
mkGVar id
| PatCstr(constr,patternl,_) ->
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
constr
in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 13ff19a46b..7b758da8e8 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function
mkGVar id
| PatCstr(constr,patternl,_) ->
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
constr
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a5c19f3217..6494e90a03 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let _ =
List.map_i
(fun i x ->
- let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
- let env = Global.env () in
+ let env = Global.env () in
+ let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in
let evd = ref (Evd.from_env env) in
let evd',uprinc = Evd.fresh_global env !evd princ in
let _ = evd := evd' in
@@ -469,11 +469,6 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
CAst.(with_val (fun x -> x))
(Constrexpr_ops.names_of_local_assums args)
in
- match wf_arg with
- | None ->
- if Int.equal (List.length names) 1 then 1
- else error "Recursive argument must be specified"
- | Some wf_arg ->
List.index Name.equal (Name wf_arg) names
in
let unbounded_eq =
@@ -575,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
in
wf_rel_with_mes,false
in
- register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes (Some wf_arg)
+ register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg
using_lemmas args ret_type body
let map_option f = function
@@ -623,15 +618,15 @@ and rebuild_nal aux bk bl' nal typ =
let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
- let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
+ let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in
let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
let constr_expr_typel =
with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
- List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
+ List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ ->
let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in
- (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixpoint_exprl constr_expr_typel
in
@@ -643,7 +638,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
let pstate, _is_struct =
match fixpoint_exprl with
- | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
+ | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] ->
let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
@@ -665,9 +660,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
true
in
if register_built
- then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, false
+ then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
else pstate, false
- |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
+ |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] ->
let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
@@ -692,9 +687,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true
else pstate, true
| _ ->
- List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
+ List.iter (function ((_na,ord,_args,_body,_type),_not) ->
match ord with
- | Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _ ->
+ | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } ->
error
("Cannot use mutual definition with well-founded recursion or measure")
| _ -> ()
@@ -869,38 +864,42 @@ let make_graph ~pstate (f_ref : GlobRef.t) =
)
()
in
- let (nal_tas,b,t) = get_args extern_body extern_type in
- let expr_list =
- match b.CAst.v with
- | Constrexpr.CFix(l_id,fixexprl) ->
- let l =
- List.map
- (fun (id,(n,recexp),bl,t,b) ->
- let { CAst.loc; v=rec_id } = Option.get n in
- let new_args =
- List.flatten
- (List.map
- (function
- | Constrexpr.CLocalDef (na,_,_)-> []
- | Constrexpr.CLocalAssum (nal,_,_) ->
- List.map
- (fun {CAst.loc;v=n} -> CAst.make ?loc @@
- CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
- nal
- | Constrexpr.CLocalPattern _ -> assert false
- )
- nal_tas
- )
- in
- let b' = add_args id.CAst.v new_args b in
- ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
- )
- fixexprl
- in
- l
+ let (nal_tas,b,t) = get_args extern_body extern_type in
+ let expr_list =
+ match b.CAst.v with
+ | Constrexpr.CFix(l_id,fixexprl) ->
+ let l =
+ List.map
+ (fun (id,recexp,bl,t,b) ->
+ let { CAst.loc; v=rec_id } = match Option.get recexp with
+ | { CAst.v = CStructRec id } -> id
+ | { CAst.v = CWfRec (id,_) } -> id
+ | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid
+ in
+ let new_args =
+ List.flatten
+ (List.map
+ (function
+ | Constrexpr.CLocalDef (na,_,_)-> []
+ | Constrexpr.CLocalAssum (nal,_,_) ->
+ List.map
+ (fun {CAst.loc;v=n} -> CAst.make ?loc @@
+ CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
+ nal
+ | Constrexpr.CLocalPattern _ -> assert false
+ )
+ nal_tas
+ )
+ in
+ let b' = add_args id.CAst.v new_args b in
+ ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ )
+ fixexprl
+ in
+ l
| _ ->
let id = Label.to_id (Constant.label c) in
- [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+ [((CAst.make id,None),None,nal_tas,t,Some b),[]]
in
let mp = Constant.modpath c in
let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..6ccf15df29 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -1,5 +1,5 @@
(library
(name recdef_plugin)
- (public_name coq.plugins.recdef)
+ (public_name coq.plugins.funind)
(synopsis "Coq's functional induction plugin")
(libraries coq.plugins.extraction))
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 3f2fabeeee..049a699cbd 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -84,7 +84,7 @@ TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
| [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
- typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] }
+ typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
END
TACTIC EXTEND head_of_constr
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7bf705ffeb..a2dd51643b 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq =
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
- | IDENT _ | INT _ ->
+ | IDENT _ | NUMERAL _ ->
(match stream_nth 2 strm with
| KEYWORD ":=" -> ()
| _ -> err ())
@@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
end
| _ -> ElimOnConstr clbind
-let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+let mkNumeral n =
+ Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n)))
let mkTacCase with_evar = function
| [(clear,ElimOnConstr cl),(None,None),None],None ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75565c1a34..2d40ba6562 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -119,7 +119,7 @@ let app_poly_check env evars f args =
(evars, cstrs), t
let app_poly_nocheck env evars f args =
- let evars, fc = f evars in
+ let evars, fc = f evars in
evars, mkApp (fc, args)
let app_poly_sort b =
@@ -175,25 +175,29 @@ end) = struct
let rewrite_relation_class = find_global relation_classes "RewriteRelation"
- let proper_class = lazy (class_info (find_reference morphisms "Proper"))
- let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
-
- let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
-
- let proper_type =
- let l = lazy (Lazy.force proper_class).cl_impl in
- fun (evd,cstrs) ->
- let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
- (evd, cstrs), c
-
- let proper_proxy_type =
- let l = lazy (Lazy.force proper_proxy_class).cl_impl in
- fun (evd,cstrs) ->
- let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
- (evd, cstrs), c
+ let proper_class =
+ let r = lazy (find_reference morphisms "Proper") in
+ fun env sigma -> class_info env sigma (Lazy.force r)
+
+ let proper_proxy_class =
+ let r = lazy (find_reference morphisms "ProperProxy") in
+ fun env sigma -> class_info env sigma (Lazy.force r)
+
+ let proper_proj env sigma =
+ mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+
+ let proper_type env (sigma,cstrs) =
+ let l = (proper_class env sigma).cl_impl in
+ let (sigma, c) = Evarutil.new_global sigma l in
+ (sigma, cstrs), c
+
+ let proper_proxy_type env (sigma,cstrs) =
+ let l = (proper_proxy_class env sigma).cl_impl in
+ let (sigma, c) = Evarutil.new_global sigma l in
+ (sigma, cstrs), c
let proper_proof env evars carrier relation x =
- let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in
+ let evars, goal = app_poly env evars (proper_proxy_type env) [| carrier ; relation; x |] in
new_cstr_evar evars env goal
let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
@@ -800,7 +804,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
in
(* Actual signature found *)
let cl_args = [| appmtype' ; signature ; appm |] in
- let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
+ let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env)
cl_args in
let env' =
let dosub, appsub =
@@ -1310,8 +1314,8 @@ module Strategies =
in
let evars, proof =
let proxy =
- if prop then PropGlobal.proper_proxy_type
- else TypeGlobal.proper_proxy_type
+ if prop then PropGlobal.proper_proxy_type env
+ else TypeGlobal.proper_proxy_type env
in
let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
new_cstr_evar evars env mty
@@ -1854,12 +1858,12 @@ let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
-let proper_projection sigma r ty =
+let proper_projection env sigma r ty =
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
let ctx, inst = decompose_prod_assum sigma ty in
let mor, args = destApp sigma inst in
let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
- let app = mkApp (Lazy.force PropGlobal.proper_proj,
+ let app = mkApp (PropGlobal.proper_proj env sigma,
Array.append args [| instarg |]) in
it_mkLambda_or_LetIn app ctx
@@ -1869,7 +1873,7 @@ let declare_projection n instance_id r =
let sigma = Evd.from_env env in
let sigma,c = Evd.fresh_global env sigma r in
let ty = Retyping.get_type_of env sigma c in
- let term = proper_projection sigma c ty in
+ let term = proper_projection env sigma c ty in
let sigma, typ = Typing.type_of env sigma term in
let ctx, typ = decompose_prod_assum sigma typ in
let typ =
@@ -1924,7 +1928,7 @@ let build_morphism_signature env sigma m =
rel)
cstrs
in
- let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
+ let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
let evd = solve_constraints env !evd in
let evd = Evd.minimize_universes evd in
let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
@@ -1938,9 +1942,9 @@ let default_morphism sign m =
let evars, _, sign, cstrs =
PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
- let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
+ let evars, morph = app_poly_check env evars (PropGlobal.proper_type env) [| t; sign; m |] in
let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
- mor, proper_projection sigma mor morph
+ mor, proper_projection env sigma mor morph
let warn_add_setoid_deprecated =
CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
@@ -1984,8 +1988,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
(None,(instance,uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
+ add_instance (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst);
pstate
else
@@ -1995,8 +1999,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
let hook _ _ _ = function
| Globnames.ConstRef cst ->
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
+ add_instance (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info
atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index caaa547a07..e617f3d45e 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x
let subst_declared_or_quantified_hypothesis _ x = x
let subst_glob_constr_and_expr subst (c, e) =
- (Detyping.subst_glob_constr subst c, e)
+ (Detyping.subst_glob_constr (Global.env()) subst c, e)
let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
@@ -99,7 +99,9 @@ let subst_evaluable subst =
let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
let subst_glob_constr_or_pattern subst (bvars,c,p) =
- (bvars,subst_glob_constr subst c,subst_pattern subst p)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p)
let subst_redexp subst =
Redops.map_red_expr_gen
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4c65445b89..d1951cc18d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
(** Test *)
let is_empty _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
- if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail
+ if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail
(* Strictly speaking, this exceeds the propositional fragment as it
matches also equality types (and solves them if a reflexivity) *)
let is_unit_or_eq _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
- if test sigma (assoc_var "X1" ist) then idtac else fail
+ if test genv sigma (assoc_var "X1" ist) then idtac else fail
let bugged_is_binary sigma t =
isApp sigma t &&
@@ -121,23 +123,25 @@ let bugged_is_binary sigma t =
(** Dealing with conjunction *)
let is_conj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let ind = assoc_var "X1" ist in
if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) &&
- is_conjunction sigma
+ is_conjunction genv sigma
~strict:flags.strict_in_hyp_and_ccl
~onlybinary:flags.binary_mode ind
then idtac
else fail
let flatten_contravariant_conj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_conjunction sigma
+ match match_with_conjunction genv sigma
~strict:flags.strict_in_contravariant_hyp
~onlybinary:flags.binary_mode typ
with
@@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist =
(** Dealing with disjunction *)
let is_disj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let t = assoc_var "X1" ist in
if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) &&
- is_disjunction sigma
+ is_disjunction genv sigma
~strict:flags.strict_in_hyp_and_ccl
~onlybinary:flags.binary_mode t
then idtac
else fail
let flatten_contravariant_disj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_disjunction sigma
+ match match_with_disjunction genv sigma
~strict:flags.strict_in_contravariant_hyp
~onlybinary:flags.binary_mode
typ with
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 38bc58a659..e12bf36339 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -141,6 +141,11 @@ Ltac IZR_tac t :=
match t with
| R0 => constr:(0%Z)
| R1 => constr:(1%Z)
+ | IZR (Z.pow_pos 10 ?p) =>
+ match isPcst p with
+ | true => constr:(Z.pow_pos 10 p)
+ | _ => constr:(InitialRing.NotConstant)
+ end
| IZR ?u =>
match isZcst u with
| true => u
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 350bb9019e..675e4d2457 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
let sort = Tacticals.elimination_sort_of_goal gl in
let gl, elim =
if not is_case then
- let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in
+ let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in
gl, t
else
Tacmach.pf_eapply (fun env sigma () ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 842e4feecf..ad20113320 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -339,7 +339,7 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
let elim, gl =
let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
let sort = elimination_sort_of_goal gl in
- let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
+ let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
let elim, _ = destConst elim in
let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
@@ -499,9 +499,9 @@ let rwprocess_rule dir rule gl =
let sigma, rs2 = loop d sigma s a.(1) rs 0 in
let s, sigma = sr sigma 1 in
loop d sigma s a.(0) rs2 0
- | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None ->
+ | App (r_eq, a) when Hipattern.match_with_equality_type env sigma t != None ->
let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in
- let np = Inductiveops.inductive_nparamdecls ind in
+ let np = Inductiveops.inductive_nparamdecls env ind in
let indu = (ind, EConstr.EInstance.kind sigma u) in
let ind_ct = Inductiveops.type_of_constructors env indu in
let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 4d65fc81d1..27a558611e 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -233,20 +233,20 @@ let test_ssrslashnum b1 b2 strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "/" ->
(match Util.stream_nth 1 strm with
- | Tok.INT _ when b1 ->
+ | Tok.NUMERAL _ when b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
| Tok.KEYWORD "/" ->
if not b2 then () else begin
match Util.stream_nth 3 strm with
- | Tok.INT _ -> ()
+ | Tok.NUMERAL _ -> ()
| _ -> raise Stream.Failure
end
| _ -> raise Stream.Failure)
| Tok.KEYWORD "/" when not b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.INT _ when b2 ->
+ | Tok.NUMERAL _ when b2 ->
(match Util.stream_nth 3 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
@@ -257,7 +257,7 @@ let test_ssrslashnum b1 b2 strm =
| Tok.KEYWORD "//" when not b1 ->
(match Util.stream_nth 1 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.INT _ when b2 ->
+ | Tok.NUMERAL _ when b2 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
@@ -369,8 +369,8 @@ let interp_index ist gl idx =
| Some c ->
let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
begin match Notation.uninterp_prim_token rc with
- | _, Constrexpr.Numeral (s,b) ->
- let n = int_of_string s in if b then n else -n
+ | _, Constrexpr.Numeral (b,{NumTok.int = s; frac = ""; exp = ""}) ->
+ let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
| _ -> raise Not_found
end
| None -> raise Not_found
@@ -1234,7 +1234,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
| [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
[Bcast t], c
| BFrec (has_str, has_cast) :: h,
- { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
+ { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
let bs = format_local_binders h bl in
let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
bs @ bstr @ (if has_cast then [Bcast t] else []), c
@@ -1458,7 +1458,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd }
| [] -> CErrors.user_err (Pp.str "Bad structural argument") in
loop (names_of_local_assums lb) in
let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
- let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in
+ let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some (CAst.make (CStructRec i))), lb, t', c']) in
id, ((fk, h'), { ac with body = fix }) }
END
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0a0d9b12fa..08f028465b 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -183,7 +183,7 @@ GRAMMAR EXTEND Gram
GLOBAL: gallina_ext;
gallina_ext:
[ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" ->
- { Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) }
+ { Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset) }
] ]
;
END
@@ -465,7 +465,7 @@ let interp_modloc mr =
(* The unified, extended vernacular "Search" command *)
let ssrdisplaysearch gr env t =
- let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in
+ let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
Feedback.msg_info (hov 2 pr_res ++ fnl ())
}
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 537fd7d7b4..075ebf006a 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -43,7 +43,7 @@ module AdaptorDb = struct
term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
let subst_adaptor ( subst, (k, t as a)) =
- let t' = Detyping.subst_glob_constr subst t in
+ let t' = Detyping.subst_glob_constr (Global.env()) subst t in
if t' == t then a else k, t'
let in_db =
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 525056e5f1..ec8c2338fb 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -56,17 +56,24 @@ let locate_z () =
}, mkRefC q_z)
else None
-let locate_int () =
+let locate_decimal () =
let int = "num.int.type" in
let uint = "num.uint.type" in
- if Coqlib.has_ref int && Coqlib.has_ref uint
+ let dec = "num.decimal.type" in
+ if Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref dec
then
let q_int = qualid_of_ref int in
let q_uint = qualid_of_ref uint in
- Some ({
+ let q_dec = qualid_of_ref dec in
+ let int_ty = {
int = unsafe_locate_ind q_int;
uint = unsafe_locate_ind q_uint;
- }, mkRefC q_int, mkRefC q_uint)
+ } in
+ let dec_ty = {
+ int = int_ty;
+ decimal = unsafe_locate_ind q_dec;
+ } in
+ Some (int_ty, mkRefC q_int, mkRefC q_uint, dec_ty, mkRefC q_dec)
else None
let locate_int63 () =
@@ -86,16 +93,16 @@ let type_error_to f ty =
CErrors.user_err
(pr_qualid f ++ str " should go from Decimal.int to " ++
pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
- fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
+ fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
let type_error_of g ty =
CErrors.user_err
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
- str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
+ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
let vernac_numeral_notation env sigma local ty f g scope opts =
- let int_ty = locate_int () in
+ let dec_ty = locate_decimal () in
let z_pos_ty = locate_z () in
let int63_ty = locate_int63 () in
let tyc = Smartlocate.global_inductive_with_alias ty in
@@ -110,11 +117,13 @@ let vernac_numeral_notation env sigma local ty f g scope opts =
let constructors = get_constructors tyc in
(* Check the type of f *)
let to_kind =
- match int_ty with
- | Some (int_ty, cint, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
- | Some (int_ty, cint, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
- | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
- | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+ match dec_ty with
+ | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
+ | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
+ | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
+ | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+ | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal dec_ty, Direct
+ | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal dec_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
@@ -127,11 +136,13 @@ let vernac_numeral_notation env sigma local ty f g scope opts =
in
(* Check the type of g *)
let of_kind =
- match int_ty with
- | Some (int_ty, cint, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
- | Some (int_ty, cint, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
- | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
- | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+ match dec_ty with
+ | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
+ | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
+ | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
+ | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+ | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal dec_ty, Direct
+ | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal dec_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index d90b7d754c..b9062dd16b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -13,6 +13,7 @@ open Names
open Globnames
open Glob_term
open Bigint
+open Constrexpr
(* Poor's man DECLARE PLUGIN *)
let __coq_plugin_name = "r_syntax_plugin"
@@ -104,22 +105,76 @@ let r_modpath = MPfile (make_dir rdefinitions)
let r_path = make_path rdefinitions "R"
let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-
-let r_of_int ?loc z =
- DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+let glob_Rmult = ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
+let glob_Rdiv = ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
+
+let binintdef = ["Coq";"ZArith";"BinIntDef"]
+let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
+
+let glob_pow_pos = ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
+
+let r_of_rawnum ?loc (sign,n) =
+ let n, f, e = NumTok.(n.int, n.frac, n.exp) in
+ let izr z =
+ DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
+ let rmult r r' =
+ DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in
+ let rdiv r r' =
+ DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in
+ let pow10 e =
+ let ten = z_of_int ?loc (Bigint.of_int 10) in
+ let e = pos_of_bignat e in
+ DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in
+ let n =
+ let n = Bigint.of_string (n ^ f) in
+ let n = match sign with SPlus -> n | SMinus -> Bigint.(neg n) in
+ izr (z_of_int ?loc n) in
+ let e =
+ let e = if e = "" then Bigint.zero else match e.[1] with
+ | '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2))
+ | '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2))))
+ | _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in
+ Bigint.(sub e (of_int (String.length f))) in
+ if Bigint.is_strictly_pos e then rmult n (izr (pow10 e))
+ else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e)))
+ else n (* e = 0 *)
(**********************************************************************)
(* Printing R via scopes *)
(**********************************************************************)
-let bigint_of_r c = match DAst.get c with
+let rawnum_of_r c = match DAst.get c with
| GApp (r, [a]) when is_gr r glob_IZR ->
- bigint_of_z a
+ let n = bigint_of_z a in
+ let s, n =
+ if is_strictly_neg n then SMinus, neg n else SPlus, n in
+ s, NumTok.int (to_string n)
+ | GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv ->
+ begin match DAst.get l, DAst.get r with
+ | GApp (i, [l]), GApp (i', [r])
+ when is_gr i glob_IZR && is_gr i' glob_IZR ->
+ begin match DAst.get r with
+ | GApp (p, [t; e]) when is_gr p glob_pow_pos ->
+ let t = bigint_of_z t in
+ if not (Bigint.(equal t (of_int 10))) then
+ raise Non_closed_number
+ else
+ let i = bigint_of_z l in
+ let e = bignat_of_pos e in
+ let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in
+ let i = Bigint.to_string i in
+ let se = if is_gr md glob_Rdiv then "-" else "" in
+ let e = se ^ Bigint.to_string e in
+ s, { NumTok.int = i; frac = ""; exp = e }
+ | _ -> raise Non_closed_number
+ end
+ | _ -> raise Non_closed_number
+ end
| _ -> raise Non_closed_number
let uninterp_r (AnyGlobConstr p) =
try
- Some (bigint_of_r p)
+ Some (rawnum_of_r p)
with Non_closed_number ->
None
@@ -131,11 +186,11 @@ let at_declare_ml_module f x =
let r_scope = "R_scope"
let _ =
- register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
+ register_rawnumeral_interpretation r_scope (r_of_rawnum,uninterp_r);
at_declare_ml_module enable_prim_token_interpretation
{ pt_local = false;
pt_scope = r_scope;
pt_interp_info = Uid r_scope;
pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
- pt_refs = [glob_IZR];
+ pt_refs = [glob_IZR; glob_Rmult; glob_Rdiv];
pt_in_match = false }
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:35:02 +0000