aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include3
-rw-r--r--dev/top_printers.ml2
-rw-r--r--interp/constrextern.ml14
-rw-r--r--interp/constrextern.mli2
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--pretyping/detyping.ml17
-rw-r--r--pretyping/retyping.ml5
-rw-r--r--pretyping/unification.ml1
-rw-r--r--printing/pptactic.ml2
-rw-r--r--test-suite/bugs/closed/3638.v25
11 files changed, 51 insertions, 24 deletions
diff --git a/dev/base_include b/dev/base_include
index 2699551a5..1d43e64df 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -210,7 +210,8 @@ let pf_e gl s =
Constrintern.interp_constr (pf_env gl) (project gl) (parse_constr s);;
(* Set usual printing since the global env is available from the tracer *)
-let _ = Constrextern.in_debugger := false
+let _ = Flags.in_debugger := false
+let _ = Flags.in_toplevel := true
let _ = Constrextern.set_extern_reference
(fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4fedbec8e..6bf294967 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -552,6 +552,6 @@ let short_string_of_ref loc _ = function
(* Anticipate that printers can be used from ocamldebug and that
pretty-printer should not make calls to the global env since ocamldebug
runs in a different process and does not have the proper env at hand *)
-let _ = Constrextern.in_debugger := true
+let _ = Flags.in_debugger := true
let _ = Constrextern.set_extern_reference
(if !rawdebug then raw_string_of_ref else short_string_of_ref)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b774da356..885b0e6b4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -158,13 +158,11 @@ let get_extern_reference () = !my_extern_reference
let extern_reference loc vars l = !my_extern_reference loc vars l
-let in_debugger = ref false
-
(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
let add_patt_for_params ind l =
- if !in_debugger then l else
+ if !Flags.in_debugger then l else
Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l
let drop_implicits_in_patt cst nb_expl args =
@@ -275,7 +273,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
not explicit application. *)
match pat with
| PatCstr(loc,cstrsp,args,na)
- when !in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
+ when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
@@ -402,7 +400,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function
let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
(* pboutill: There are letins in pat which is incompatible with notations and
not explicit application. *)
- if !in_debugger||Inductiveops.inductive_has_local_defs ind then
+ if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
let c = extern_reference Loc.ghost vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
CPatCstr (Loc.ghost, c, add_patt_for_params ind args, [])
@@ -438,7 +436,7 @@ let occur_name na aty =
| Anonymous -> false
let is_projection nargs = function
- | Some r when not !in_debugger && not !Flags.raw_print && !print_projections ->
+ | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
(try
let n = Recordops.find_projection_nparams r + 1 in
if n <= nargs then None
@@ -731,7 +729,7 @@ let rec extern inctx scopes vars r =
(na',Option.map (fun (loc,ind,nal) ->
let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
let fullargs =
- if !in_debugger then args else
+ if !Flags.in_debugger then args else
Notation_ops.add_patterns_for_params ind args in
extern_ind_pattern_in_scope scopes vars ind fullargs
) x))) tml in
@@ -944,7 +942,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
(* those goal/section/rel variables that occurs in the subterm under *)
(* consideration; see namegen.ml for further details *)
let avoid = if goal_concl_style then ids_of_context env else [] in
- let r = Detyping.detype ~lax goal_concl_style avoid env sigma t in
+ let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in
let vars = vars_of_env env in
extern false (scopt,[]) vars r
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 023c5be22..804795480 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -59,8 +59,6 @@ val set_extern_reference :
val get_extern_reference :
unit -> (Loc.t -> Id.Set.t -> global_reference -> reference)
-val in_debugger : bool ref
-
(** This governs printing of implicit arguments. If [with_implicits] is
on and not [with_arguments] then implicit args are printed prefixed
by "!"; if [with_implicits] and [with_arguments] are both on the
diff --git a/lib/flags.ml b/lib/flags.ml
index 0356863ab..a744ce9b0 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -73,6 +73,8 @@ let async_proofs_is_master () =
!async_proofs_mode = APon && !async_proofs_worker_id = "master"
let debug = ref false
+let in_debugger = ref false
+let in_toplevel = ref false
let profile = false
diff --git a/lib/flags.mli b/lib/flags.mli
index f94d80ffc..e53de166d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,8 @@ val string_of_priority : priority -> string
val priority_of_string : string -> priority
val debug : bool ref
+val in_debugger : bool ref
+val in_toplevel : bool ref
val profile : bool
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 823f5ef64..d691acb45 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -438,15 +438,14 @@ let rec detype flags avoid env sigma t =
(Array.map_to_list (detype flags avoid env sigma) args)
| Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
| Proj (p,c) ->
- (try
- let ty = Retyping.get_type_of (snd env) sigma c in
- let (ind, args) = Inductive.find_rectype (snd env) ty in
- GApp (dl, GRef (dl, ConstRef p, None),
- List.map (detype flags avoid env sigma) (args @ [c]))
- with e when fst flags (* lax mode, used by debug printers only *) ->
- GApp (dl, GRef (dl, ConstRef p, None),
- [detype flags avoid env sigma c])
- | e -> raise e)
+ if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
+ (* lax mode, used by debug printers only *)
+ GApp (dl, GRef (dl, ConstRef p, None),
+ [detype flags avoid env sigma c])
+ else let ty = Retyping.get_type_of (snd env) sigma c in
+ let (ind, args) = Inductive.find_rectype (snd env) ty in
+ GApp (dl, GRef (dl, ConstRef p, None),
+ List.map (detype flags avoid env sigma) (args @ [c]))
| Evar (evk,cl) ->
let id,l =
try Evd.evar_ident evk sigma,
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index c7bdabe93..8f1a16dce 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -126,8 +126,9 @@ let retype ?(polyprop=true) sigma =
(subst_type env sigma (type_of env f) (Array.to_list args))
| Proj (p,c) ->
let Inductiveops.IndType(pars,realargs) =
- try Inductiveops.find_rectype env sigma (type_of env c)
- with Not_found -> anomaly ~label:"type_of" (str "Bad recursive type")
+ let ty = type_of env c in
+ try Inductiveops.find_rectype env sigma ty
+ with Not_found -> retype_error BadRecursiveType
in
let (_,u), pars = dest_ind_family pars in
substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7b302229b..d03fd8521 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1325,6 +1325,7 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) =
with
| PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
raise (NotUnifiable (Some (c1,c2,e)))
+ (** MS: This is pretty bad, it catches Not_found for example *)
| e when Errors.noncritical e -> raise (NotUnifiable None) in
let merge_fun c1 c2 =
match c1, c2 with
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 841eb6039..bd4e9d93e 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -342,7 +342,7 @@ let pr_ltac_or_var pr = function
| ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
let pr_ltac_constant kn =
- if !Constrextern.in_debugger then pr_kn kn
+ if !Flags.in_debugger then pr_kn kn
else try
pr_qualid (Nametab.shortest_qualid_of_tactic kn)
with Not_found -> (* local tactic not accessible anymore *)
diff --git a/test-suite/bugs/closed/3638.v b/test-suite/bugs/closed/3638.v
new file mode 100644
index 000000000..70144174d
--- /dev/null
+++ b/test-suite/bugs/closed/3638.v
@@ -0,0 +1,25 @@
+(* File reduced by coq-bug-finder from original input, then from 7593 lines to 243 lines, then from 256 lines to 102 lines, then from 104 lines to 28 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 17 2014 0:22:30 with OCaml 4.01.0
+ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d34e1eed232c84590ddb80d70db9f7f7cf13584a) *)
+Set Primitive Projections.
+Set Implicit Arguments.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+Class UnitSubuniverse := { O : Type -> Type ; O_unit : forall T, T -> O T }.
+Class ReflectiveSubuniverse := { rsubu_usubu : UnitSubuniverse ; O_rectnd : forall {P Q : Type} (f : P -> Q), O P -> Q }.
+Global Existing Instance rsubu_usubu.
+Context {subU : ReflectiveSubuniverse}.
+Goal forall (A B : Type) (x : O A * O B) (x0 : B),
+ { g : _ & O_rectnd (fun z : A * B => (O_unit (fst z), O_unit (snd z)))
+ (O_rectnd (fun a : A => O_unit (a, x0)) (fst x)) =
+ g x0 }.
+ eexists.
+ Show Existentials. Set Printing Existential Instances.
+ match goal with
+ | [ |- context[?e] ] => is_evar e; let e' := fresh "e'" in set (e' := e)
+ end.
+
+
+(* Toplevel input, characters 15-114:
+Anomaly: Bad recursive type. Please report. *) \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 08:11:12 +0000