diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 12:53:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
| commit | 105db906ae45e792d1caeeb2e3fb7f69944b2caa (patch) | |
| tree | b12ca28e6b172d2524c6a11c851c7d568f6a2411 /pretyping/recordops.mli | |
| parent | b17c1e128fad2e84ebe4e4742b47bd67d88c56d6 (diff) | |
- Fixes for canonical structure resolution (check that the initial term indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
Diffstat (limited to 'pretyping/recordops.mli')
| -rw-r--r-- | pretyping/recordops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index b1763a359..4a03d9bc5 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -66,7 +66,7 @@ type obj_typ = { val cs_pattern_of_constr : constr -> cs_pattern * int * constr list val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds -val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ +val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ val declare_canonical_structure : global_reference -> unit val is_open_canonical_projection : Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool |