diff options
| -rw-r--r-- | pretyping/typing.ml | 6 | ||||
| -rw-r--r-- | pretyping/typing.mli | 5 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_074.v | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_114.v | 1 | ||||
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_074.v | 12 | ||||
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_114.v | 2 |
7 files changed, 19 insertions, 19 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 5cd05c58d..2f34f7efe 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -285,11 +285,13 @@ let sort_of env evd c = (* Try to solve the existential variables by typing *) -let e_type_of env evd c = +let e_type_of ?(refresh=false) env evd c = let evdref = ref evd in let j = execute env evdref c in (* side-effect on evdref *) - !evdref, j.uj_type + if refresh then + Evarsolve.refresh_universes false !evdref j.uj_type + else !evdref, j.uj_type let solve_evars env evdref c = let c = (execute env evdref c).uj_val in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8b194a9c9..26dc8c560 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -17,8 +17,9 @@ open Evd (** Typecheck a term and return its type *) val type_of : env -> evar_map -> constr -> types -(** Typecheck a term and return its type + updated evars *) -val e_type_of : env -> evar_map -> constr -> evar_map * types +(** Typecheck a term and return its type + updated evars, optionally refreshing + universes *) +val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Typecheck a type and return its sort *) val sort_of : env -> evar_map -> types -> sorts diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0d2b3d5a1..69505172c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -650,7 +650,7 @@ let interp_may_eval f ist env sigma = function str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - sigma , Typing.type_of env sigma c_interp + Typing.e_type_of ~refresh:true env sigma c_interp | ConstrTerm c -> try f ist env sigma c diff --git a/test-suite/bugs/closed/HoTT_coq_074.v b/test-suite/bugs/closed/HoTT_coq_074.v new file mode 100644 index 000000000..370c7d404 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_074.v @@ -0,0 +1,10 @@ +Monomorphic Definition U1 := Type. +Monomorphic Definition U2 := Type. + +Set Printing Universes. +Definition foo : True. +let t1 := type of U1 in +let t2 := type of U2 in +idtac t1 t2; +pose (t1 : t2). exact I. +Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v new file mode 100644 index 000000000..341128338 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_114.v @@ -0,0 +1 @@ +Inductive test : $(let U := type of Type in exact U)$ := t. diff --git a/test-suite/bugs/opened/HoTT_coq_074.v b/test-suite/bugs/opened/HoTT_coq_074.v deleted file mode 100644 index 7c88447b2..000000000 --- a/test-suite/bugs/opened/HoTT_coq_074.v +++ /dev/null @@ -1,12 +0,0 @@ -Monomorphic Definition U1 := Type. -Monomorphic Definition U2 := Type. - -Set Printing Universes. -Definition foo : True. -Fail let t1 := type of U1 in -let t2 := type of U2 in -pose (t1 : t2). (* Error: -The term "Type (* Top.1+1 *)" has type "Type (* Top.1+2 *)" -while it is expected to have type "Type (* Top.2+1 *)". *) -exact I. -Defined. diff --git a/test-suite/bugs/opened/HoTT_coq_114.v b/test-suite/bugs/opened/HoTT_coq_114.v deleted file mode 100644 index e293e6dbb..000000000 --- a/test-suite/bugs/opened/HoTT_coq_114.v +++ /dev/null @@ -1,2 +0,0 @@ -Fail Inductive test : $(let U := type of Type in exact U)$ := t. -(* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *) |