Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Thanks to Peter Lumsdaine for bug reporting:

- fix externalisation of universe instances (still appearing when no Printing Universes)
- add [convert] and [convert_leq] tactics that keep track of evars and universe constraints.
- use them in [exact_check].
  • Loading branch information...
commit 07f38ce8602a26fad421bf43dac4d4a7bb18032c 1 parent 6dadbfa
@mattam82 mattam82 authored
View
8 interp/constrextern.ml
@@ -683,6 +683,10 @@ let extern_glob_sort = function
| GType (Some _) as s when !print_universes -> s
| GType _ -> GType None
+let extern_universes = function
+ | Some _ as l when !print_universes -> l
+ | _ -> None
+
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
try
@@ -696,7 +700,7 @@ let rec extern inctx scopes vars r =
with No_match -> match r' with
| GRef (loc,ref,us) ->
extern_global loc (select_stronger_impargs (implicits_of_global ref))
- (extern_reference loc vars ref) us
+ (extern_reference loc vars ref) (extern_universes us)
| GVar (loc,id) -> CRef (Ident (loc,id),None)
@@ -757,7 +761,7 @@ let rec extern inctx scopes vars r =
| Not_found | No_match | Exit ->
extern_app loc inctx
(select_stronger_impargs (implicits_of_global ref))
- (Some ref,extern_reference rloc vars ref) us args
+ (Some ref,extern_reference rloc vars ref) (extern_universes us) args
end
| _ ->
explicitize loc inctx [] (None,sub_extern false scopes vars f)
View
2  pretyping/reductionops.ml
@@ -637,7 +637,7 @@ let trans_fconv pb reds env sigma x y =
Evd.add_constraints sigma cst, true
with NotConvertible -> sigma, false
| Anomaly _ -> error "Conversion test raised an anomaly"
-
+
(********************************************************************)
(* Special-Purpose Reduction *)
(********************************************************************)
View
16 tactics/tactics.ml
@@ -119,6 +119,16 @@ let convert_concl = Tacmach.convert_concl
let convert_hyp = Tacmach.convert_hyp
let thin_body = Tacmach.thin_body
+let convert_gen pb x y gl =
+ try tclEVARS (pf_apply Evd.conversion gl pb x y) gl
+ with Reduction.NotConvertible ->
+ let env = pf_env gl in
+ tclFAIL 0 (str"Not convertible: " ++ Printer.pr_constr_env env x ++
+ str" and " ++ Printer.pr_constr_env env y) gl
+
+let convert = convert_gen Reduction.CONV
+let convert_leq = convert_gen Reduction.CUMUL
+
let error_clear_dependency env id = function
| Evarutil.OccurHypInSimpleClause None ->
errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
@@ -1095,10 +1105,8 @@ let cut_and_apply c gl =
let exact_check c gl =
let concl = (pf_concl gl) in
let ct = pf_type_of gl c in
- if pf_conv_x_leq gl ct concl then
- refine_no_check c gl
- else
- error "Not an exact proof."
+ try tclTHEN (convert_leq ct concl) (refine_no_check c) gl
+ with _ -> error "Not an exact proof." (*FIXME error handling here not the best *)
let exact_no_check = refine_no_check
View
2  tactics/tactics.mli
@@ -54,6 +54,8 @@ val mutual_fix :
val fix : identifier option -> int -> tactic
val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic
val cofix : identifier option -> tactic
+val convert : constr -> constr -> tactic
+val convert_leq : constr -> constr -> tactic
(** {6 Introduction tactics. } *)
View
9 toplevel/command.ml
@@ -290,6 +290,13 @@ let interp_ind_arity evdref env ind =
(* let _ = evdref := Evd.abstract_undefined_variables !evdref in *)
make_conclusion_flexible evdref ty; (ty, impls)
+let normalize_arity_universes evdref env params inds =
+ let subst = Evarutil.evd_comb0 Evd.nf_constraints evdref in
+ let nf = Universes.subst_univs_full_constr subst in
+ let arities = List.map (fun (ty, impls) -> make_conclusion_flexible evdref ty, impls) inds in
+ let params = Sign.map_rel_context nf params in
+ params, arities
+
let interp_cstrs evdref env impls mldata arity ind =
let cnames,ctyps = List.split ind.ind_lc in
(* Complete conclusions of constructor types if given in ML-style syntax *)
@@ -375,6 +382,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly finite =
(* Interpret the arities *)
let arities = List.map (interp_ind_arity evdref env_params) indl in
+ (* let ctx_params, arities = normalize_arity_universes evdref ctx_params arities in *)
+
let fullarities = List.map (fun (c, _) -> it_mkProd_or_LetIn c ctx_params) arities in
let env_ar = push_types env0 indnames fullarities in
let env_ar_params = push_rel_context ctx_params env_ar in
Please sign in to comment.
Something went wrong with that request. Please try again.