diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 02:22:59 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:05:40 -0400 |
| commit | a15e584571a4e153e98a11c93d12759c45ea2dcd (patch) | |
| tree | ecb28582eef51f801e2440f715715dda1b6bb06b /vernac/comFixpoint.ml | |
| parent | affb6ac843380e8e134fd89380746f2f6f8c11de (diff) | |
[proof] [mutual] Factorize universe handling.
Note that we had to introduce a `restrict_ucontext` parameter to be
faithful to the implementation in obligations, however this looks like
a bug.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 6e6be4fe3a..0e2d8c1453 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,24 +255,20 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - let possible_indexes, cofix, fix_kind = +let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = + let possible_indexes, fix_kind = match indexes with - | Some indexes -> Some indexes, false, Decls.(IsDefinition Fixpoint) - | None -> None, true, Decls.(IsDefinition CoFixpoint) + | Some indexes -> Some indexes, Decls.(IsDefinition Fixpoint) + | None -> None, Decls.(IsDefinition CoFixpoint) in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let univs = Evd.check_univ_decl ~poly evd pl in - let ubind = Evd.universe_binders evd in let _ : GlobRef.t list = - DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind ~ntns - fixnames fixdecls fixtypes fiximps + DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx + ~possible_indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration + fixnames fixtypes fiximps in () |