diff options
Diffstat (limited to 'tuto3/src')
| -rw-r--r-- | tuto3/src/tuto_tactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml index cb73a4486b..9818867621 100644 --- a/tuto3/src/tuto_tactic.ml +++ b/tuto3/src/tuto_tactic.ml @@ -15,7 +15,7 @@ let collect_constants () = let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in - constants := List.map (fun x -> of_constr (constr_of_global x)) + constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x)) [gr_H; gr_M; gr_R; gr_P; gr_U]; !constants else |