diff options
| author | herbelin | 2012-01-27 22:07:57 +0000 |
|---|---|---|
| committer | herbelin | 2012-01-27 22:07:57 +0000 |
| commit | 0bfefe15d6c174c60cc0eb50a54254c20228f30e (patch) | |
| tree | 0593e4f0fd310a47e74fc47757d706ff2be93d51 | |
| parent | c51a32a5f3825dfd78212c976fb0d2d62b4e7d71 (diff) | |
Printing bugs with match patterns:
- namegen.ml: if a matching variable has the same name as a constructor,
rename it, even if the conflicting constructor name is defined in a
different module;
- constrextern.ml: protect code for printing cases as terms are from
requesting info in the global env when printers are called from ocamldebug
since the global env is undefined in this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/constrextern.ml | 23 | ||||
| -rw-r--r-- | pretyping/namegen.ml | 2 |
2 files changed, 16 insertions, 9 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index be60c9c307..bd8e78c0f5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -140,14 +140,19 @@ let extern_evar loc n l = let debug_global_reference_printer = ref (fun _ -> failwith "Cannot print a global reference") +let in_debugger = ref false + let set_debug_global_reference_printer f = + in_debugger := true; debug_global_reference_printer := f let extern_reference loc vars r = - try Qualid (loc,shortest_qualid_of_global vars r) - with Not_found -> - (* happens in debugger *) + if !in_debugger then + (* Debugger does not have the tables of global reference at hand *) !debug_global_reference_printer loc r + else + Qualid (loc,shortest_qualid_of_global vars r) + (************************************************************************) (* Equality up to location (useful for translator v8) *) @@ -371,7 +376,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = try - if !Flags.raw_print then raise Exit; + if !in_debugger || !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = match projs with @@ -388,15 +393,17 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = CPatRecord(loc, List.rev (ip projs args [])) with Not_found | No_match | Exit -> + let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in + if !in_debugger then CPatCstr (loc, c, args) else if !Topconstr.oldfashion_patterns then if pattern_printable_in_both_syntax cstrsp - then CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) - else CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), add_patt_for_params cstrsp args) + then CPatCstr (loc, c, args) + else CPatCstrExpl (loc, c, add_patt_for_params cstrsp args) else let full_args = add_patt_for_params cstrsp args in match drop_implicits_in_patt cstrsp full_args with - |Some true_args -> CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), true_args) - |None -> CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), full_args) + |Some true_args -> CPatCstr (loc, c, true_args) + |None -> CPatCstrExpl (loc, c, full_args) in insert_pat_alias loc p na and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 2ad2f3515c..abb6b510d1 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -53,7 +53,7 @@ let is_global id = let is_constructor id = try match locate (qualid_of_ident id) with - | ConstructRef _ as ref -> not (is_imported_ref ref) + | ConstructRef _ -> true | _ -> false with Not_found -> false |