diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-15 19:19:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-15 19:22:40 +0200 |
| commit | 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 (patch) | |
| tree | 7c5f1ef4a58575566b36a4b1f58f4acb26f95396 /toplevel | |
| parent | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (diff) | |
Allow `Pretyping.search_guard` to not check guard
This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.
Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 3 |
2 files changed, 6 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index b6dd2718f..c4f0b7b17 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1065,7 +1065,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let env = Global.env() in - let indexes = search_guard Loc.ghost env indexes fixdecls in + let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = @@ -1169,7 +1169,9 @@ let do_program_recursive local p fixkind fixl ntns = Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = - Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in + Pretyping.search_guard + ~tflags:{Declarations.check_guarded=true} + Loc.ghost (Global.env ()) possible_indexes fixdecls in List.iteri (fun i _ -> Inductive.check_fix env ~flags:{Declarations.check_guarded=true} diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 9df5a411b..ec58392d5 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -582,7 +582,8 @@ let declare_mutual_definition l = List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in let indexes = - Pretyping.search_guard Loc.ghost (Global.env()) + Pretyping.search_guard ~tflags:{Declarations.check_guarded=true} + Loc.ghost (Global.env()) possible_indexes fixdecls in Some indexes, List.map_i (fun i _ -> |