diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-10 15:17:20 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:15:49 +0200 |
| commit | a79481b86881be12900b9b16b2f384eb3c402215 (patch) | |
| tree | 4b4a65fc0d1ae5aedb32c8e386164468d1ab2f48 /plugins/romega/refl_omega.ml | |
| parent | 0fe4d837191de481184cc995558ca3774253be0c (diff) | |
romega: discard constructor D_mono (shorter trace + fix a bug)
For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
Diffstat (limited to 'plugins/romega/refl_omega.ml')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index bb4ab37ff..af396d489 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1029,8 +1029,11 @@ let find_path {o_hyp=id;o_path=p} env = let mk_direction_list l = let trans = function - O_left -> coq_d_left | O_right -> coq_d_right | O_mono -> coq_d_mono in - mk_list (Lazy.force coq_direction) (List.map (fun d-> Lazy.force(trans d)) l) + | O_left -> Some (Lazy.force coq_d_left) + | O_right -> Some (Lazy.force coq_d_right) + | O_mono -> None (* No more [D_mono] constructor now *) + in + mk_list (Lazy.force coq_direction) (List.map_filter trans l) (* \section{Rejouer l'historique} *) @@ -1156,13 +1159,10 @@ and decompose_tree_hyps trace env ctxt = function with Not_found -> failwith (Printf.sprintf "Cannot find equation %d" i) in let (index,path) = find_path equation.e_origin ctxt in - let full_path = if equation.e_negated then path @ [O_mono] else path in let cont = decompose_tree_hyps trace env (CCEqua equation.e_omega.id :: ctxt) l in - app coq_e_extract [|mk_nat index; - mk_direction_list full_path; - cont |] + app coq_e_extract [|mk_nat index; mk_direction_list path; cont |] (* \section{La fonction principale} *) (* Cette fonction construit la |