diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-27 19:20:27 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-27 19:20:27 +0000 |
| commit | 11ca3113365639136cf65a74c345080a9434e69b (patch) | |
| tree | da263c149cd1e90bde14768088730e48e78e4776 /plugins/quote | |
| parent | ee2f85396fa0cef65bc4295b5ac6c259e83df134 (diff) | |
Removing a bunch of generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index c09e2d743..92b27c3e8 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -207,7 +207,7 @@ let compute_lhs typ i nargsi = let compute_rhs bodyi index_of_f = let rec aux c = match kind_of_term c with - | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) -> + | App (j, args) when isRel j && Int.equal (destRel j) index_of_f (* recursive call *) -> let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> @@ -239,7 +239,7 @@ let compute_ivs gl f cs = (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *) (* REL 1 to REL nargsi are argsi (reverse order) *) (* First we test if the RHS is the RHS for constants *) - if isRel bodyi && destRel bodyi = 1 then + if isRel bodyi && Int.equal (destRel bodyi) 1 then c_lhs := Some (compute_lhs (snd (List.hd args3)) i nargsi) (* Then we test if the RHS is the RHS for variables *) @@ -260,7 +260,7 @@ let compute_ivs gl f cs = end) lci; - if !c_lhs = None && !v_lhs = None then i_can't_do_that (); + if Option.is_empty !c_lhs && Option.is_empty !v_lhs then i_can't_do_that (); (* The Cases predicate is a lambda; we assume no dependency *) let p = match kind_of_term p with @@ -338,8 +338,8 @@ let path_of_int n = (* returns the list of digits of n in reverse order with initial 1 removed *) let rec digits_of_int n = - if n=1 then [] - else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + if Int.equal n 1 then [] + else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1)) in List.fold_right (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx |