Library MetaCoq.Template.config

Class checker_flags := {
  

  
  check_univs : bool ;

  
  prop_sub_type : bool ;

  
  indices_matter : bool ;

  
  lets_in_constructor_types : bool
}.

Local Instance default_checker_flags : checker_flags := {|
  check_univs := true ;
  prop_sub_type := true;
  indices_matter := false;
  lets_in_constructor_types := true
|}.

Local Instance type_in_type : checker_flags := {|
  check_univs := false ;
  prop_sub_type := true;
  indices_matter := false;
  lets_in_constructor_types := true
|}.

Local Instance extraction_checker_flags : checker_flags := {|
  check_univs := true ;
  prop_sub_type := false;
  indices_matter := false;
  lets_in_constructor_types := false
|}.