let debug_print s =
if debug then prerr_endline (Lazy.force s);;
+let is_propositional context sort =
+ match CicReduction.whd context sort with
+ | Cic.Sort Cic.Prop
+ | Cic.Sort (Cic.CProp _) -> true
+ | _-> false
+;;
+
+
type auto_params = Cic.term list * (string * string) list
let elems = ref [] ;;
CicTypeChecker.type_of_aux' metasenv context mt
CicUniv.oblivion_ugraph
in
- let b, _ =
- CicReduction.are_convertible ~metasenv context
- sort (Cic.Sort Cic.Prop) u
- in
- if b then Some i else None
+ if is_propositional context sort then Some i else None
| _ -> assert false)
args
in
CicTypeChecker.type_of_aux' metasenv context mt
CicUniv.oblivion_ugraph
in
- let b, _ =
- CicReduction.are_convertible ~metasenv context
- sort (Cic.Sort Cic.Prop) u
- in
- if b then Some i else None
+ if is_propositional context sort then Some i else None
| _ -> assert false)
args
in
;;
let is_in_prop context subst metasenv ty =
let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
- fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+ is_propositional context sort
;;
let assert_proof_is_valid proof metasenv context goalty =
let _,context,ty = CicUtil.lookup_meta g metasenv in
try
let sort,u = typeof ~subst metasenv context ty ugraph in
- let b,_ =
- CicReduction.are_convertible
- ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
- b
+ is_propositional context sort
with
| CicTypeChecker.AssertFailure s
| CicTypeChecker.TypeCheckerFailure s ->
let order_new_goals metasenv subst open_goals ppterm =
let prop,rest = split_goals_in_prop metasenv subst open_goals in
let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
+ let closed_type, open_type = split_goals_with_metas metasenv subst rest in
let open_goals =
- (List.map (fun x -> x,P) (closed_prop @ open_prop))
+ (List.map (fun x -> x,P) (open_prop @ closed_prop))
@
- (List.map (fun x -> x,T) rest)
+ (List.map (fun x -> x,T) (open_type @ closed_type))
in
let tys =
List.map